Ssreflect Users Discussion List

[Georges Gonthier <>]

     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<---------------------------------------------------