The Coq mailing list

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

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.

Regards.