The Coq mailing list

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

On 16/12/2016 09:50, Ralf Jung wrote:
> Hi,
> 
>>> it
>>> seems like it's actually searching for "X.foo" in one go, and there
>>> could be multiple modules X that it is checking here?
>>
>> Correct
> 
> Well, that's what I meant by merging, I guess.  Or maybe it is
> backtracking on what module "X" refers to.

There is no backtracking involved. Try to imagine instead that all the
symbols known by Coq at a given time are stored in a large search tree
with each edge being labeled with an identifier. At each node of the
tree, there is at most one symbol, that is why there is no backtrack.

But there is one peculiarity. When following a path in the search tree,
a qualified name is being read from right to left. Whenever you import a
module, you overwrite a bunch of nodes of the search tree.

So when searching for "X.foo", Coq first follows the edge "foo", then
the edge "X", and there it finds a single symbol (or none, but certainly
not several ones).

Best regards,

Guillaume