Search code examples
coqcoqide

coqc: -Q.PLF: no such file or directory

I am trying to compile a file hw5.v in coq which is in the plf folder of software foundations. I want to resolve the bindings and hence I use the command :

coqc -Q.PLF hw5.v

But it does not compile and gives the error as coqc: -Q.PLF: no such file or directory. This has never happened before. If I do man coqc or coqc -v, it gives me the correct output. But it is not working with -Q or -R. Any idea to resolve this? my coq version is : 8.9.1

Solution

  • (Putting the answer from the comments to close the question.)

    The correct command is coqc -Q . PLF hw5.v, so that -Q, . and PLF are different arguments to the command-line program coqc.