The Coq mailing list

[sidi <Sidi.Ould_Biha AT inria.fr>]

Hi Laurent,

Using Navigation does not allow to remove the induction principle
defined by Coq. A solution is to use CoInductive à la SSreflect or PG :)

Regards
On Thu, 2010-06-10 at 10:32 +0200, Laurent Théry wrote:
> 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