The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Le 04/02/2015 19:04, Pierre Courtieu a écrit :
> 2015-02-04 18:31 GMT+01:00 Frédéric Blanqui 
> <frederic.blanqui AT inria.fr>:
> > Hello.
> >
> > Thank you for your answers.
> >
> > 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 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. Not fixing this 
bug may lead people to use a flat file structure for their libraries 
which does not seem very nice. Frédéric.


> > Best regards,
> >
> > Frédéric.