Search code examples
coqcoqide

`Reset` not working in CoqIDE

Neither Reset <sectionname>. nor Reset <globalconstant>. nor Reset Initial. works in my CoqIDE interactive sessions. The message is

Error: Use CoqIDE navigation instead

The only Resets I've seen to work are Reset Extraction Blacklist. and Reset Extraction Inline.. Below's a copy of some info from Help > About. Thanks in advance for any ideas

**Version information**

The Coq Proof Assistant, version 8.4pl3 (January 2014)  
Architecture Linux running Unix operating system
Gtk version is 2.24.23  
This is coqide.opt (opt is the best one for this architecture and OS)
Solution

  • If you are willing to upgrade to Coq 8.5, CoqIDE now supports Reset, Undo, Abort, Restart... It will just print a warning advising you to use navigation commands instead when you use them.