The Coq mailing list

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

Hi Frédéric, here is what I understand, people will correct me if I am wrong.

This is a complex question since you may not be the author of the
libraries. Ideally each library should be compiled with option -R (or
the new -Q option, but it is broken currently in 8.5beta). Then
compiling L1 should give for example:

coqc -R L1 L1 L1/F.v

same for L2:

coqc -R L2 L2 L2/F.v

and the two "make install" should do the equivalent of:

cp L1/F.vo lib/coq/user-contrib/L1/
cp -r L2/F.vo lib/coq/user-contrib/L2/

Then "L1.F" and "L2.F" should work OK.

Of course the libraries need to be adapted to these compilation
options, they should "Require L1.F" themselves for example. If you
didn't write the library yourself you may need to 1) modify it to be
compilable this way or 2) contact the author of the library and ask
him to adopt this kind of compilation discipline.

P.




2015-02-04 16:33 GMT+01:00 Frédéric Blanqui 
<frederic.blanqui AT inria.fr>:
> Hello.
>
> If I install two distinct Coq libraries L1 and L2 in lib/coq/user-contrib/
> (default with coq_makefile) and each one contains a file F.v, how do I do to
> distinguish them in Coq?
>
> Cheers,
>
> Frédéric.
>