The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

Why not just add an additional distinct syntactic element for
unambiguous usage? Something such as:

Strict Requrie Foo.bar.baz.

Then leave the Coq library requires as is, and let users decide whether
they want to continue to deal with ambiguous requires in their own
libraries or use the new unambiguous one.

On Fri, 18 Sep 2020 17:30:24 +0200
Guillaume Melquiond <guillaume.melquiond AT inria.fr> wrote:

> Le 18/09/2020 à 17:05, Ralf Jung a écrit :
> > So it sounds to me like the standard library was not designed very
> > well in terms of module names (no blame here, these things are much
> > easier to realize in hindsight), and then to work around that
> > language semantics were adjusted? That does not sound very
> > principled.  
> 
> At some point, you have to be pragmatic and decide that aggravating
> your users is not worth having a more principled language. Here is a
> concrete example that happened just a few days ago.
> 
> Here is a question I could have added to my previous quiz:
> 
> 6.a Require Coq.ring.Ring.
> 6.b Require Coq.setoid_ring.Ring.
> 
> As it happens, a Coq developer decided to remedy this discrepancy a
> few days ago. Guess what? It broke about one quarter of the user
> libraries we test in Coq's continuous integration.
> 
> It did not take long to decide that this change would just aggravate
> users and was not worth it, despite being principled.
> 
> Best regards,
> 
> Guillaume