CODEWITHSUNDEEP
coqcoqide
jaam
jaam

Reputation: 970

`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)

Upvotes: 0

Views: 332

Answers (2)

Zimm i48
Zimm i48

Reputation: 3061

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.

Upvotes: 1

Vinz
Vinz

Reputation: 6047

From what I remember, the Reset action is just the "go to the top of the file and forget everything" arrow, the one that backtracks the whole file. This message is here to prevent weird behavior by mixing such commands with IDE bindings of CoqIde

Edit after comments: There is no real concept of "global" variables in Coq: it's a functional programming language. You have access to anything that is defined prior to you. It can be in the same module or in an imported module.

If you want to get rid of a top level declaration in the same module, the only way I know is to move the definition down up to the point you really need it. If it is in an external module you imported, the only solution is not to import the module.

I might be wrong, please do not hesitate to correct me. My understanding is that removing such a definition forces you to remove anything that depends on this definition, which is not a simple task to perform.

Upvotes: 0

Related Questions