我在mac os X上使用CoqIDE_8.4pl5.当CoqIDE转发到此命令时,会弹出此错误消息:需要导入基础.
错误:编译库Basics.vo对库Coq.Init.Notations进行不一致的假设
当我使用CoqIDE_8.4pl5时,我没有在我的旧Macbook Air上遇到此问题,但是当我得到一个新的macbook pro时,我又从同一个网站下载了它.但是这次在这个macbook pro上,我使用brew cask install coq来安装它...但它似乎不起作用,所以我从网站上下载并将我的coqide路径设置为我在旧macbook中的相同路径air ..当我尝试转发我的作业时,我遇到了这个问题.有没有什么办法解决这一问题？或者我是否必须删除coq并复制并重新安装？
coq ×1