The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 01/06/2015 03:56 PM, Peter LeFanu Lumsdaine wrote:
> Normally, to disambiguate between objects with the same short name, one can
> refer to them by their absolute names.  E.g. if the working directory
> contains identically-named library files in different subdirectories,
> Dir1/MyMod.vo and Dir2/MyMod.vo, compiled with module names Dir1.MyMod and
> Dir2.MyMod, then issuing
>
> Add Rec LoadPath ".".
> Require Import MyMod.
>
> might load either, but one can specify which by giving the absolute name: [
> Require Import Dir1.MyMod. ] or [ Require Import Dir2.MyMod. ]
>
>
> But if there is also a MyMod.vo in the working directory itself (compiled
> with module name MyMod), then its absolute name is just [ Mymod ], but in [
> Require Import MyMod ], Coq still interprets [MyMod ] as an ambiguous short
> name, not as an absolute name.  In this situation, is there any way to tell
> Coq that we want the module with absolute name [ MyMod ], not the modules
> from the subdirectories?

I think the "Top." prefix always works for anchoring absolute names: 
Top.MyMod

-- Jonathan