相关疑难解决方法(0)

我无法加载CoqIde中相同文件夹中的模块.

我试图从软件基金会加载来源,我跑在包含SF sources文件夹coqide coqide或coqide ./,然后打开并运行该文件后,我得到这个错误:

Error: Cannot find library Poly in loadpath

在这一行:

Require Export Poly.

并且对于其他所有require命令都是一样的.

那么你们如何将程序从SF加载到coqide？