coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Guillaume Melquiond <guillaume.melquiond AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] option to disable partially qualified Require Imports
- Date: Thu, 17 Sep 2020 17:01:00 +0200
Le 17/09/2020 à 16:19, Abhishek Anand a écrit :
> I used to think that using disjoint logical prefixes for different
> libraries and always using fully qualified names in Require Imports
> would suffice for avoiding errors due to incorrect files being imported.
> However, it was recently pointed out to me that this is not sufficient:
> Suppose we have 2 .vo files, one with fully qualified name A.B.C and
> another with fully qualified name B.C.
> Now we suddenly have no reliable way to Import the latter file unless
> there is a way to tell `Require Import` that the name should be
> interpreted in a fully qualified manner.
> Is there a workaround for this?
You can use:
From A Require B.C.
From B Require C.
If you have three files named A.C, A.B.C, and B.A.C, then there is no
foolproof way to load A.C. But this is the author of library A being
malicious. Just stop using library A.
Best regards,
Guillaume
- [Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Gregory Malecha, 09/17/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Gaëtan Gilbert, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Guillaume Melquiond, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Abhishek Anand, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Gaëtan Gilbert, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Théo Zimmermann, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/18/2020
- Re: [Coq-Club] option to disable partially qualified Require Imports, Ralf Jung, 09/17/2020
Archive powered by MHonArc 2.6.19+.