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

Question

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

coqc -Q.PLF hw5.v

但是它不会编译，并显示错误，如coqc：-Q.PLF：没有这样的文件或目录。这从未发生过。如果执行man coqc或coqc -v，它会给我正确的输出。但它不适用于-Q或-R。有解决的办法吗？我的CoQ版本是：8.9.1

Answer 1

（从评论中输入答案以结束问题。）

正确的命令是coqc -Q . PLF hw5.v，因此-Q，.和PLF是命令行程序coqc的不同参数。