The Coq mailing list

[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. 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
>