The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

Hi again,

I strongly recommend you never use Add LoadPath. Instead, you should use a _CoqProject file containing a single -R or -Q directive. From there you can use coq_makefile to generate a Makefile to compile your project. The _CoqProject file is also understood by Proof General and CoqIDE, so from there it should all work out of the box.

I would link you to the documentation, but I'm on my phone so it's a bit difficult.

Théo

Le mar. 3 sept. 2019 à 20:44, Karl Crary <crary AT andrew.cmu.edu> a écrit :

Hmm.  This doesn't quite seem to do what I want.  I'm trying:

Add LoadPath "." as Here.
 From Here Require Import Foo.

and I get:

The file .../Foo.vo contains library Foo and not library Here.Foo

        -- Karl Crary


On 9/3/2019 12:34 PM, Théo Zimmermann wrote:
> Hi,
>
> If the collision occurs at Require Import time, you can use the From
> prefix to specify that the module should be found in your own project
> instead of Coq's library.
> Cf. https://coq.inria.fr/refman/proof-engine/vernacular-commands.html#coq:cmdv.require-import
>
> Théo
>
> Le mar. 3 sept. 2019 à 18:31, Karl Crary <crary AT andrew.cmu.edu> a écrit :
>>
>> Hi all,
>>
>> I upgraded to 8.9.1, and found that several new modules have been added
>> to the library whose names collide with my own.  Unfortunately, this
>> breaks my code in many places.  Is there a way to tell Coq to give
>> precedence to local sources over libraries?
>>
>> Thanks for any help.
>>
>>          -- Karl Crary
>>