Ltac не работает после обновления до Coq 8.5

Question

У меня есть следующий Ltac ( отсюда), который работал на Coq 8.4pl6, но он не работает на 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.

Я получил сообщение об ошибке

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

Я не знаю достаточно о Ltac. Может кто-нибудь помочь объяснить, как это исправить?

Answer 1

В Coq 8.5 Arith определяет обозначение =?, Из-за этого, что было интерпретировано как = ?B теперь интерпретируется как =? B, Добавление пробела между = а также ?B должно быть достаточно.