The Coq mailing list

[Johannes Waldmann <johannes AT albapasser.de>]

> > 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 [...]

I just noticed a similar problem in Java:
new Foo.Bar.Baz () could mean either of

package Foo; class Bar { static class Baz { } }; // in Foo/Bar.java
package Foo.Bar; class Baz { };           // in Foo/Bar/Baz.java

it is in fact an error (flagged by the compiler)
to compile the second version if the first version is present.
(but not the other way round - strangely)

I think this refusal to compile is right (much better
than compiling and then complaining about ambiguous imports)

Best regards, Johannes Waldmann.