Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] option to disable partially qualified Require Imports

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] option to disable partially qualified Require Imports


Chronological Thread 
  • 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



Archive powered by MHonArc 2.6.19+.

Top of Page