为什么Coquelicot会弄乱我的子弹？
假设我在 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.
似乎导入 from 的行为Coquelicot使得项目符号点被完全忽略。几个问题：
- 为什么会发生这种情况？这是某种错误吗？
- 有没有办法禁用这种行为？我想使用 Coquelicot 并且仍然要检查正确的项目符号使用情况。
我目前使用的是用 OCaml 4.10.2 和 Coquelicot 3.2.0 编译的 Coq 8.13.2。
回答
Coquelicot 依赖于 MathComp，而 MathComp 禁用了项目符号的传统含义（因为它们的使用方式不同）。但是，它们不是在 MathComp 项目本地执行此操作，而是全局设置一个选项，这就是您获得此行为的原因。
要检索预期的行为，您需要将选项重置为默认值，如下所示：
Set Bullet Behavior "Strict Subproofs".
（参见https://coq.inria.fr/refman/proofs/writing-proofs/proof-mode.html#coq:opt.Bullet-Behavior）