The Coq mailing list

[Laurent Théry <Laurent.Thery AT sophia.inria.fr>]

sidi wrote:
> Hi,
>
> When Replaying some coq scripts in CoqIDE, I got an error message after
> the execution a Reset in a context similar to the flowing :
> Inductive toto : Type :=
>   | A : toto
>   | B : toto -> toto.
>
> Reset toto_rect.
> ...
> Error: Use CoqIDE navigation instead
>
> If this is not a CoqIDE bug, I don't see why the user should get an
> error msg.
>
>   

CoqIde doesn't accept Reset commands. To do reset you should use navigation
instead (put you cursor to the definition you want to undo and click on 
go to cursor).

--
Laurent