Search code examples
coqltac

Ltac not working after upgrading to Coq 8.5

I have the following Ltac (from here), which used to work on Coq 8.4pl6, but it's not working on Coq 8.5 beta 3:

Ltac maybe_intro_sym A B :=
  match goal with
    |[H:B=A|-_] => fail 1
    |[H:A=B|-_] => assert (B=A) by auto
  end.

Ltac maybe_intro_sym_neg A B :=
  match goal with
    |[H:B<>A|-_] => fail 1
    |[H:A<>B|-_] => assert (B<>A) by auto
  end.

Ltac intro_sym :=
  repeat match goal with
    |[H:?A=?B|-_] => maybe_intro_sym A B
    |[H:?A<>?B|-_] => maybe_intro_sym_neg A B
end.

I got an error message saying

Error: The reference B was not found
in the current environment.

I don't know enough about Ltac. Can anyone help explain how to fix this?

Solution

  • In Coq 8.5, Arith defines the notation =?. Because of this, what was interpreted as = ?B is now interpreted as =? B. Adding a space between = and ?B should be enough.