The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

If you really need to use such commands, you can use proofgeneral,
which do not check commands written in the buffer. However be warned
that the backtracking mechanism of navigation commands will be
completely confused.

I suppose that the same behavior could be added to coqide via a
special option (demowithoutbacktrack?). With the same drawbacks.

Regards,
Pierre

2010/3/6 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.
>