The Coq mailing list

[Adam Chlipala <adamc AT csail.mit.edu>]

Well, then I guess I'm allowed to advertise for the idea of proving each 
theorem with a single tactic. :)

It's not obvious to me that new tactic notations don't do more harm than 
good, when they retain most of the unreadability disadvantages of more 
traditional approaches.

Alexandre Pilkiewicz wrote:
> And here is the point where I advertise for my Case tactics :)
>
> https://github.com/pilki/cases/blob/master/test-suite/case_tactics_ex.v
>
> Cheers,
> Alexandre
>
> On Mon, Nov 14, 2011 at 9:13 AM, Pierre Courtieu
> <Pierre.Courtieu AT cnam.fr>
>   wrote:
>    
> > Hello,
> >
> > There is a chance that more structuring syntax will come up in future
> > versions of coq. For example in trunk you have the experimental
> > keywords "BeginSubProof." (in short "{") and "EndSubProof." ("}").
> > There is also an experimental "bullets" system inspired from ssreflect
> > (although quite different). So you can expect to have scripts looking
> > like this in the future:
> >
> > assert (Q x).
> >   { split.
> >    + intro.
> >       auto.
> >    + auto. }
> > auto.
> >
> > note this is still very experimental and it is neither completely
> > decided nor working yet.
> >
> > Note moreover that this has nothing to do with any declarative mode:
> > bullets and curly brackets are nothing more than slightly different
> > versions of Focus and Unfocus.
> >
> > Pierre
> >
> >