coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] name conflicts between coq libraries

From: Jason Gross <jasongross9 AT gmail.com>
To: coq-club <coq-club AT inria.fr>
Subject: Re: [Coq-Club] name conflicts between coq libraries
Date: Wed, 4 Feb 2015 11:58:06 -0500

I think you can do [Require Import L1.F.] and [Require Import L2.F].

-Jason

On Feb 4, 2015 10:34 AM, "Frédéric Blanqui" <frederic.blanqui AT inria.fr> wrote:

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.

[Coq-Club] name conflicts between coq libraries, Frédéric Blanqui, 02/04/2015
- Re: [Coq-Club] name conflicts between coq libraries, Jason Gross, 02/04/2015
- Re: [Coq-Club] name conflicts between coq libraries, Pierre Courtieu, 02/04/2015
  - Re: [Coq-Club] name conflicts between coq libraries, Guillaume Melquiond, 02/04/2015
    - Re: [Coq-Club] name conflicts between coq libraries, Frédéric Blanqui, 02/04/2015
      - Re: [Coq-Club] name conflicts between coq libraries, Pierre Courtieu, 02/04/2015
        
        Re: [Coq-Club] name conflicts between coq libraries, Frédéric Blanqui, 02/04/2015
        
        Re: [Coq-Club] name conflicts between coq libraries, Guillaume Melquiond, 02/04/2015
    - Re: [Coq-Club] name conflicts between coq libraries, Pierre Courtieu, 02/04/2015