The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

On Thu, Dec 12, 2013 at 4:38 AM, Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

Still, I would add a small exception to the non-recursiveness. If a path happens to point to a directory rather than a file, a file with that name inside the directory should be selected. For instance, to load the Coquelicot library, the user should only have to do "Require Coquelicot" rather than "Require Coquelicot.Coquelicot".

What should the behavior be if there is a module whose absolute path is  Foo.Bar.Bar?  Should we be able to import it as Foo.Bar?  That is, should the above exception only apply to the top level, or should it also apply to subdirectories?

I also think that Coq should separate it's namespacing and it's directory structure, and/or allow mix-in modules (namespaces) that are merged rather than shadowed.  (See, e.g., https://coq.inria.fr/bugs/show_bug.cgi?id=3171)

-Jason