coq - 升级到 Coq 8.5 后 Ltac 无法正常工作

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。=在and之间添加一个空格?B就足够了。