Ssreflect Users Discussion List

[Christian Doczkal <>]

Thanks for the quick reply. I was wondering not so much about uncaught side 
conditions but rather about the 'focusing' behavior of Coq's bullets. I guess 
I'll just wait for Enrico to return from his vacation.

Regards
Christian

On 11.09.2012, at 13:22, Georges Gonthier <> wrote:

>     Hi Christian,
>  I'm afraid the short answer is no. You would have to write your own 
> plug-in to re-shadow the ssreflect bullets with the Coq 8.4 ones.
> The semantics of Coq bullets is essentially incompatible with their 
> established use in the ssreflect library, as a complement to indentation -- 
> indeed it is rather pointless to check bullets but not indentation, and 
> anyway this check would be better done by the IDE rather than the system.
>   If you're using ssreflect, then paragraph termination is checked by the 
> 'by' tactical so the bullet check is mostly redundant. The exception to 
> this is that bullets will catch unproved side conditions that were 
> generated after the main goal of a tactic -- a situation that can occur, 
> e.g., after
>    rewrite subnK //.
> if the 'cut' // fails to catch the m <= n side condition; indeed such rogue 
> side conditions can go undetected for some time, which is a hassle when 
> reworking proofs. Coq bullets don't help much here, because the main issue 
> is that rogue side conditions go undetected in long straight-line tactic 
> sequences...
>  The real culprit here is the error-prone subgoal order of the rewrite 
> tactic, and ssreflect 1.4 actually corrects this historical error, though 
> for now this is disabled by default via the OldSsrRewriteGoalsOrder user 
> option (and we haven't ported the library to the new order). You are 
> encouraged to experiment with the new order, which will become the default 
> in future releases.  
> 
>    Cheers,
> Georges
> 
> (Note: the  ssreflect plugin code does try to disable the bullet behaviour 
> "cleanly" via the undocumented Unset Bullet Behavior user option, but AFAIR 
> this did not work for some reason and we still had to override the grammar 
> rule. Enrico might give you a more precise answer when he returns from 
> holiday in two weeks' time.)
> 
> 
> -----Original Message-----
> From: Christian Doczkal [] 
> Sent: 11 September 2012 11:03
> To: 
> Subject: Coq Bullets vs. Ssreflect Bullets
> 
> 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<---------------------------------------------------
>