The Coq mailing list

[Catalin Hritcu <catalin.hritcu AT gmail.com>]

This is a real pity. Adam Chlipala's online book on Certified
Programming with Dependent Types (http://adam.chlipala.net/cpdt/) uses
"Restart" and "Abort" extensively.

Wish you a great day,
Catalin


On Thu, Mar 4, 2010 at 8:38 PM, Pierre Courtieu 
<Pierre.Courtieu AT cnam.fr>
 wrote:
> 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. The locked region is supposed to represent at any time
> the definitions already accepted by the prover. In particular allowing
> such command would lead to situations where navigation forward would
> be impossible. For example:
>
>
> Definition X:=nat.
> (*Point 2*)
> Definition Y := X.
> Definition Z:= ....
> Reset X.
> (* Point 1*)
>
> Suppose the user navigates this file to point  1 and then back to
> point 2, then definition of Y is not typable since X was resetted. So
> the user is stuck.
>
> This may seem restrictive but I think it is a good thing that this
> kind of problem is avoided.
>
> However it may be interesting to wish for an option for disabling this
> restriction for people knowing what they do.
>
> You may use proofgeneral for that in the meantime, though I would not
> call this a feature of PG...
>
> Regards,
> People
>
>
> 2010/3/4 
> �<catalin.hritcu AT gmail.com>:
>> Hello,
>>
>> I have an apparently similar problem with the commands "Restart" and 
>> "Abort".
>> They are accepted by coqc, but CoqIDE gives out an "Error: Use CoqIDE
>> navigation instead". "Reset" doesn't work either.
>>
>> Is it possible that this is a CoqIDE bug?
>>
>> Thanks,
>> Catalin
>>
>