The Coq mailing list

[Adam Chlipala <adam AT chlipala.net>]

Pierre Courtieu wrote:
> Why not use comments to keep track failed attempts?
>
> Pierre
>
> 2010/3/5 Damien 
> Pous<Damien.Pous AT ens-lyon.fr>:
>    
> > 2010/3/4 Pierre 
> > Courtieu<Pierre.Courtieu AT cnam.fr>:
> >      
> > > No this is not a bug. These commands are supposed to be used when
> > > using coq in a terminal. Using these command in coqide would
> > > de-synchronize the "locked region" of the buffer and coq typing
> > > environment.
> > >        
> > What about "Abort", which does not raise such a problem (I think) ?
> > (I find Abort quite useful, to keep track of failed attempts.)
> >      

That works well for most cases, but it's not so nice for preparing 
educational materials, such that you want your automated build process 
to check that the "failed attempts" still work as expected.