The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

Le mer. 20 janv. 2021 à 13:14, Jeremy Dawson
<Jeremy.Dawson AT anu.edu.au> a écrit :
> that the -Q and -R options have these two distinct
> purpose?

Yes It serves these two purposes at the same time: it tells how to
compile .v and where to look for .vo.

>  In which case, I suppose you say
> coqc -Q ... xx genT.v
> (but what goes in the place of the ...)
> and if you need to use say
> coqc -Q XX xx -Q YY yy genT.v
> does the file genT.vo contain library xx.genT or yy.genT?

No. Because in your example genT.v does not seem to be in directory xx
or yy, so the two -Q commands do not affect it.

But if genT.v is in a directory foo, then
coqc -Q YY yy -Q foo xx foo/genT.v
will build foo/genT.vo with logical name xx.genT. And during the
compilation a file YY/f.vo will be accessible with name  "yy.f" *and
should have be compiled to comply with this*.

Hope this helps.

> Thanks
>
> Jeremy