我想在对当前项目进行编码时导入我的一个项目的文件。
即导入文件/中的ProjectA/fileA.v/fileB.v.
我如何通过配置Makefile或_Coqproject来做到这一点。
在_CoqProject:的开头添加以下行
-R ../ProjectA SomeName
然后你应该能够写
From SomeName Require Import fileA.