Ltac升级到Coq 8.5后不起作用

Question

我有以下Ltac (来自here)，它以前在CoQ8.4pl6上工作，但它不在CoQ8.5beta 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

在CoQ8.5中，Arith定义了表示法=?。正因为如此，被解释为= ?B的东西现在被解释为=? B。在=和?B之间添加一个空格就足够了。