The Coq mailing list

[frederic.blanqui AT loria.fr]

On Tue, 3 Jun 2008, Johannes Waldmann wrote:

> I was starting with the naive expectation that "Require Foo.Bar.Baz"
> leads to reading the file Foo/Bar/Baz.v(o)

note that such a policy may create new ambiguities:

if you have a file Foo.v in which you define a Module Bar in which you define 
a module Baz,

and a directory Foo in which you have a file Bar.v in which you define a 
module Baz.