The Coq mailing list

[Maxime Dénès <mail AT maximedenes.fr>]

Hi Théo,

I fully agree with your advice, by why don't we deprecate `Add
LoadPath`, then?

Maxime.

On 9/3/19 10:59 PM, Théo Zimmermann wrote:
> 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
> <mailto: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
>     
> <mailto: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
>     >>
>