`Reset` 在 CoqIDE 中不起作用

Question

Reset <sectionname>.、Reset <globalconstant>. 和 Reset Initial. 在我的 CoqIDE 交互会话中都不起作用。消息是

Error: Use CoqIDE navigation instead

我见过唯一有效的 Reset 是 Reset Extraction Blacklist. 和 Reset Extraction Inline.。以下是“帮助”>“关于”中的一些信息的副本。提前感谢任何想法

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

Answer 1

根据我的记忆，Reset 操作就是 "go to the top of the file and forget everything" 箭头，即回溯整个文件的箭头。此消息是为了通过将此类命令与 CoqIde

的 IDE 绑定混合来防止奇怪的行为

评论后编辑： Coq 中没有 "global" 变量的真正概念：它是一种函数式编程语言。您可以访问之前定义的任何内容。它可以在同一个模块中，也可以在导入的模块中。

如果你想去掉同一模块中的顶级声明，我知道的唯一方法是将定义向下移动到你真正需要它的地方。如果它在你导入的外部模块中，唯一的解决办法就是不导入该模块。

可能我说的不对，请大家指正。我的理解是删除这样的定义会强制您删除依赖于此定义的任何内容，这不是一项简单的任务。

Answer 2

如果您愿意升级到 Coq 8.5，CoqIDE 现在支持 Reset、Undo、Abort、Restart...它只会打印一条警告，建议您在使用导航命令时改用导航命令。

`Reset` 在 CoqIDE 中不起作用

`Reset` not working in CoqIDE

coq

coqide