The Coq mailing list

[Peter LeFanu Lumsdaine <p.l.lumsdaine AT gmail.com>]

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?

(Actually, in case it makes a difference, in my use-case the module that is shadowing my [ ./MyMod.vo ] is not in a subdirectory of the working directory; it’s an external library, which has been added to the LoadPath via [ coqtop -R … ].)

Many thanks,

–Peter.

(Some relevant sections of reference manual: 2.6 https://coq.inria.fr/refman/Reference-Manual004.html#sec95 , 6.5, 6.6 https://coq.inria.fr/refman/Reference-Manual008.html#sec264 .)