The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

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.

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