The Coq mailing list

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

2015-02-04 18:15 GMT+01:00 Guillaume Melquiond 
<guillaume.melquiond AT inria.fr>:
>> (or the new -Q option, but it is broken currently in 8.5beta).
> Oh?

In presence of subdirectories in the library, it does not produce the
correct module names (#3958).

>> Of course the libraries need to be adapted to these compilation
>> options, they should "Require L1.F" themselves for example.
>
> Only if they are being compiled using -Q. If they are compiled using -R,
> they do not need to (unless there is an ambiguity inside a library itself).

True. The point is that if one changes the compilation options then
the Requires may have to be changed in the files. So libraries authors
should always release there libraries with -R or -Q and a good (i.e.
unique) name.
"Lib", "Tactics" or "Common" should be banned :).

P.

> Best regards,
>
> Guillaume