The Coq mailing list

[Gert Smolka <smolka AT ps.uni-saarland.de>]

Thanks,  curly braces for tree-structuring proofs are in fact exactly what I 
want. When should I expect the release of v8.4?

Am 15.11.2011 um 11:07 schrieb Pierre Boutillier:

> There is a command to do something like that. It is
> BeginSubproof.
> 
> EndSubproof.
> (Moreover, it also checks if you've really solve the subgoal)
> 
> Why am I talking about that wheareas it is much longer than
> Focus 1
> 
> Focus 1
> 
> because in trunk
> BeginSubproof is {
> and EndSubproof is }
> 
> CoqIde and proof general are ready for that (It is the Proof General 
> maintener that has introduiced the feature) but you'll have to be patient 
> and wait for v8.4 (that would not come soon if we follow Mr Porton 
> reccommendation :-D)
> 
> Pierre
> PS : In trunk, you could also try the bullet things (+/-/*) but the work 
> for them hasn't been done until the end and they are not parsed alone so 
> you often have to write + idtac in order to remember your goal...
> 
> Le 15 nov. 11 à 10:22, Gert Smolka a écrit :
> 
>> Can I switch Coq's subgoal display in a mode where it shows only the 
>> current subgoal?  The command Focus does it, but I have to reenter "Focus" 
>> whenever I switch do a new goal, and I don't want to write "Focus" in my 
>> scripts.  I'm working with Proof General.