如何解决coq后缀导入错误(绑定到逻辑路径的物理路径)

Question

可能是一个coq新手问题,但我找不到一个现成的解决方案,所以我会在这里请求参考.cocq版本是8.5pl2

我试着建立 coqfj.第一次make尝试失败,第37行出现了一些错误src/FJ/ClassTable.v.这个问题不是关于那个错误.

仔细看看,我打开ClassTable.v了emacs proofgeneral并按下C-c C-n,或者运行coqc src/FJ/ClassTable.v.结果是第1行出错:

File "./src/FJ/ClassTable.v", line 1, characters 15-23:
Error: Cannot find a physical path bound to logical path matching suffix FJ.

似乎导入require import FJ.Lists无法解决(尽管FJ用作前缀,而不是后缀).我注意到make已经创建了一个编译文件src/Lists.vo,应该由coqc选中.

如何告诉coqc它应该通过查看文件夹中的文件*.vo或*.v文件来解决这个"后缀" src？