我正在使用CoqIDE来完成有关Coq的《软件基础》一书中的练习。我可以成功编译Basics.v，从而在我的目录中生成Basics.vo和Basics.glob。当我尝试运行Induction.v时，它可以工作。当我尝试编译它时，它提示缺少大量引用，例如evenb和negb_involutive。如果我将Basics.v的内容复制到Induction.v中，它将进行编译，但是显然这不是可行的方法。
这不是问题Coq error: The reference evenb was not found in the current environment的重复项，因为我已经做了这些事情:
编译Basics.v。检查Basics.vo是否在目录中。现在编译Induction.v。最后一步失败。
最佳答案
我自己遇到了这个错误。尝试从Software Foundations文件所在的目录打开CoqIDE，然后从那里编译。如果您使用的是Linux，只需打开一个终端，转到该目录，然后在其中键入coqide。我不知道如何在其他系统上执行此操作，例如Mac OS，但我确实注意到，仅通过图标打开应用程序会导致应用程序失败。
关于coq - 在当前环境中找不到引用 “X”，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/40129401/