coq - coqc: -Q.PLF: 没有这样的文件或目录

Question

我正在尝试在软件基础的 plf 文件夹中的 coq 中编译文件 hw5.v。我想解决绑定，因此我使用命令：

coqc -Q.PLF hw5.v

但它不会编译并给出错误为 coqc: -Q.PLF: no such file or directory。这是以前从未发生过的。如果我执行 man coqc 或 coqc -v，它会给我正确的输出。但它不适用于 -Q 或 -R。有什么办法解决这个问题吗？我的 coq 版本是：8.9.1

标签： coqcoqide

Answer 1

（从评论中给出答案以结束问题。）

正确的命令是,coqc -Q . PLF hw5.v所以和是命令行程序的不同参数。-Q.PLFcoqc