Ssreflect Users Discussion List

[Christian Doczkal <>]

Hello

Ssreflect has had bullets for quite some time time. Coq 8.4 introduces 
bullets of its own that share the Ssreflect syntax but also perform focusing 
and check that subgoals are closed before moving to the next bullet. It 
appears that upon importing ssreflect, the ssreflect bullets shadow coq's 
bullets. 

Is there a way to disable Ssreflect's bullets but keep all the other syntax 
modifications of ssreflect?

Are there any incompatibilities to be aware of?

Regards
Christian


-------------------------8<------------------------------------------------
(using Proofgeneral 4.2pre120814)

Goal forall b: bool , b = b.
intros [].
- reflexivity.
- reflexivity.
Qed.

Require Import ssreflect.

Goal forall b: bool , b = b.
intros [].
- reflexivity.
- reflexivity.
Qed.

-------------------------8<---------------------------------------------------