The Coq mailing list

[<ncyms8r3x2 AT snkmail.com>]

I tried using importing Coquelicot library and I noticed the bullets  (-, +,
and *) started behaving differently. For example, coq would suddenly accept
this:
    Theorem simple: True /\ True.
    Proof.
      + +
      split.
      - exact I.
      - exact I.
    Qed.

It turns out that Coquelicot includes ssreflect, and ssreflect calls 'Set
Bullet Behavior "None".'

I searched the reference manual and mailing list archives, but I didn't find
any references to this option. So FYI, you can restore the default behavior
with:
    Set Bullet Behavior "Strict Subproofs".