The Coq mailing list

[Christian Doczkal <christian.doczkal AT inria.fr>]

Hi

> Anyhow, I've tried your suggestion:  I assume "-R/-Q" means choose
> either "-R" or "-Q" (without assuming this, coq_makefile produces errors).

Yes.

> Then coq_makefile seems to work OK but then "make" produces the following
> 
> lots of warnings of which I show the last
> *** Warning: in file modal/k4.v, library lntacsT is required and has not
> been found in the loadpath!
> COQC lnt/tense-logic-in-Coq/cut_extraction_test.v

Ah sorry, the syntax of -R and -Q is [-R physicalpath logicalpath] so
all three -R/-Q lines need a logical path as well (i.e., the prefix you
use in "From <prefix> Require Import <lib>). Something like TL, gen,...)

The difference between -R and -Q is IIRC whether the files inside the
folder use the prefix when including other files from the same folder or
not.

> Error: Invalid character '-' at beginning of identifier "-Q".
> make[1]: *** [Makefile:657:
> lnt/tense-logic-in-Coq/cut_extraction_test.vo] Error 1
> make: *** [Makefile:318: all] Error 2

make is trying to use -Q as logical path, which obviously fails ...

Hope this helps!
Christian