The Coq mailing list

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

Le 18/09/2020 à 14:18, Gaëtan Gilbert a écrit :
> We perhaps could add a syntax with leading dot, so in
> 
>     Require .Foo.Bar Baz.
> 
> Foo.Bar is fully qualified, Baz isn't.
> 
> (kind of like internet domain names with trailing dot)

Another possibility would be to relax some requirements of From-Require.
Currently, "From A.B.C Require D.E.F" means that not only the path
should start with A.B.C and finish with D.E.F, but also that there
should be no overlap between A.B.C and D.E.F. If the second constraint
was removed, then Require would become non-ambiguous for people who have
to use messy libraries.

Best regards,

Guillaume