coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] name conflicts between coq libraries

From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
To: coq-club AT inria.fr
Subject: [Coq-Club] name conflicts between coq libraries
Date: Wed, 04 Feb 2015 16:33:56 +0100

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