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

如果您愿意升级到Coq8.5，CoqIDE现在支持重置、撤消、中止、重新启动.当您使用导航命令时，它只会打印警告，建议您使用导航命令。

Answer 2

据我所知，Reset操作仅仅是“转到文件的顶部，忘记所有的东西”箭头，一个回溯整个文件的箭头。此消息的目的是通过将这些命令与CoqIde的IDE绑定混合起来，从而防止这种奇怪的行为。

注释后编辑:Coq中没有真正的“全局”变量的概念:它是一种函数式编程语言。您可以访问在您之前定义的任何内容。它可以在相同的模块中，也可以在导入的模块中。

如果您想摆脱同一个模块中的顶级声明，我知道的唯一方法就是将定义向下移动到您真正需要的程度。如果它位于您导入的外部模块中，则唯一的解决方案是不导入该模块。

我可能错了，请不要犹豫地纠正我。我的理解是，删除这样的定义会迫使您删除任何依赖于此定义的内容，这并不是一项简单的任务。