The Coq mailing list

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

Le 18/09/2020 à 16:46, Ralf Jung a écrit :
> (Probably the
> language designer had a good reason and this was solving a concrete 
> problem, but
> putting the blame on the library is just unfair. And you haven't argued for 
> why
> Coq's semantics make any sense, either.)

The reason is the standard library of Coq. It is important to understand
how painful it would be to use if Imports had to be fully qualified.
Here is a quiz for you. Which of the following are correct?

1.a Require Coq.List.List.
1.b Require Coq.Lists.List.

2.a Require Coq.Reals.Reals.
2.b Require Coq.Reals.Real.

3.a Require Coq.Derive.Derive.
3.b Require Coq.derive.Derive.

4.a Require Coq.Btauto.Btauto.
4.b Require Coq.btauto.Btauto.

5.a Require Coq.String.String.
5.b Require Coq.Strings.String.

So, when we introduced the From-Require syntax, we decided that the user
should never have to learn all these idiosyncrasies, which we have to
preserve for backward compatibility.

Sure, if you are using your own standard library, then you do not need
to bother about it. But Coq's developers do not have this luxury.

Best regards,

Guillaume