Why does Coquelicot mess with my bullets?

Question

Suppose I write the following lemma and proof in Coq:

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

The simpl here doesn't do anything, and this is a bad use of bullet points (-). When I try to compile this with coqc, I get the following complaint:

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

It's clear to me why this error happens. When I open the second bullet point for auto, it complains that I didn't finish the first bullet point. However, what doesn't make sense to me is that this code compiles fine:

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

It seems that the act of importing from Coquelicot makes it so that bullet points are completely ignored. A couple questions:

• Why does this happen? Is this some sort of bug?
• Is there a way to disable this behavior? I would like to use Coquelicot and still have proper bullet point usage be checked.

I'm currently using Coq 8.13.2 compiled with OCaml 4.10.2, and Coquelicot 3.2.0.

Catechism

Answer 1

Coquelicot depends on MathComp and MathComp disables the conventional meaning of bullets (because they use them differently). However, instead of doing this locally to the MathComp project, they set an option globally, and that's why you get this behavior.

To retrieve the expected behavior, you need to reset the option to the default value like this:

Set Bullet Behavior "Strict Subproofs".

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

Ostmark