Ltac not working after upgrading to Coq 8.5

1
votes

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?

1
coqltac
There is no problem for me. Which of the three Ltac definitions sends this error ? – eponier
@eponier It's the last one intro_sym. – thor
Are you sure that it's not something stupid such as an unbreakable space after one of the B ? – eponier
Yes, it seems strange that it shouldn't work.... Have you copied and pasted it from the page? Or could there be a missing '?' before the B in the pattern? (The pattern is what's before the '=>') (Note that only intro_sym should have question marks, as it should match any _ = _ term, but the others shouldn't, as they should only match the specific term with the given A and B) – larsr
I have copy-and-pasted the above into a library file SfLib.v from described and available from cis.upenn.edu/~bcpierce/sf/current/SfLib.html to be included in other .v files. This worked on Coq 8.4pl6 without a problem, but gave me the quoted error when 8.5beta3 is used. I am not sure if it could be a conflict with content in that file, but otherwise things are copy-pasted without missing a white space. – thor

1 Answers

2
votes

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.