0

在我的CoqIDE交互式会话中既不Reset <sectionname>.也不工作。消息是Reset <globalconstant>.Reset Initial.

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

2 回答 2

1

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

于 2016-04-21T11:43:10.393 回答
0

据我所知，该Reset操作只是“转到文件顶部并忘记所有内容”箭头，即回溯整个文件的箭头。此消息旨在通过将此类命令与 CoqIde 的 IDE 绑定混合来防止奇怪的行为

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

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

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

于 2016-03-29T06:56:50.123 回答