The Coq mailing list

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

On 04/02/2015 21:25, Frédéric Blanqui wrote:

> > > However, I notice that, if the file F.v of L1 is in a subdirectory,
> > > say D,
> > > then L1.F does not work. Instead we need to use L1.D.F.
> > True. It looks like a bug. Note that D.F works however (unless hidden
> > by another D).
> > P.
> Good to hear that because it doesn't seem a desirable feature

Actually, unless I am misunderstanding the issue at hand, this is the 
expected behavior. The logical path of your file is L1.D.F, so the 
allowed paths to load it are F, D.F, and L1.D.F.

> since it
> exposes the internal file structure of the library to the outside:
> renaming a directory or moving a file into another directory will have
> an impact to all developments depending on this library.

Sure, but that is also true if you rename a file. If your users can cope 
with file renaming, they can also cope with directory renaming.

> Not fixing this
> bug may lead people to use a flat file structure for their libraries
> which does not seem very nice.

My suggestion would be to design your library so that the user never has 
to directly include files hidden deep into your library. For instance, 
you should have a few files at the toplevel of the library that exports 
all the other files.

Best regards,

Guillaume