coq - 为什么 Coquelicot 会弄乱我的子弹？

Question

假设我在 Coq 中写出以下引理和证明:

Lemma foo : forall A, A -> A.
Proof.
  - simpl.
  - auto.
Qed.

simpl这里什么也不做，这是对要点的错误使用( - )。当我尝试用 coqc 编译它时，我收到以下投诉:

Error: [Focus] Wrong bullet -: Current bullet - is not finished.

我很清楚为什么会发生这个错误。当我打开 auto 的第二个要点时，它提示我没有完成第一个要点。但是，对我来说没有意义的是这段代码编译得很好:

From Coquelicot Require Import Complex.
Lemma foo : forall A, A -> A.
Proof.
  - simpl.
  - auto.
Qed.

似乎是从 Coquelicot进口的行为使得项目符号点被完全忽略。几个问题:

为什么会发生这种情况？这是某种错误吗？

有没有办法禁用这种行为？我想使用 Coquelicot 并且仍然要检查正确的项目符号使用情况。

我目前使用的是用 OCaml 4.10.2 和 Coquelicot 3.2.0 编译的 Coq 8.13.2。

Answer 1

Coquelicot 依赖于 MathComp，而 MathComp 禁用了项目符号的传统含义(因为它们的使用方式不同)。但是，它们不是在 MathComp 项目本地执行此操作，而是全局设置一个选项，这就是您获得此行为的原因。
要检索预期的行为，您需要将选项重置为默认值，如下所示:

Set Bullet Behavior "Strict Subproofs".

(参见 https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Bullet-Behavior)