The Coq mailing list

[Guillaume Melquiond <guillaume.melquiond AT inria.fr>]

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