The Coq mailing list

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

On 23/08/2016 18:27, Pierre Courtieu wrote:
> 2016-08-23 16:54 GMT+02:00 Guillaume Melquiond 
> <guillaume.melquiond AT inria.fr>:
>> On 23/08/2016 16:15, Beta Ziliani wrote:
>>> Hi list,
>>>
>>> We've been fighting this issue for way too long, and now it's time to
>>> ask the crowd. We like to override the notation for lists /only/ when
>>> the list is the argument of certain definition. However, the notation is
>>> being pervasive to every list. Aren’t scopes intended for that? What is
>>> wrong with our understanding of scopes?
> 
>> Open scopes only control whether you need to explicitly tell Coq which
>> interpretation scope to use (using %scope). They have no impact on
>> whether a notation is enabled or disabled (be it for parsing or printing).
> 
> However intuitively one would think that when printing the choice of
> notation is the one that needs no % at parsing (top of the scope
> stack). And this is not the case.

While I might get convinced that it would be better to start looking for
a notation using the scopes that are currently stacked (before looking
into other scopes), I would not go as far as qualifying this behavior as
"intuitive".

The current behavior is more or less to select the most recent notation.
In particular, if there is a notation in the current file, it will take
precedence over notations defined in other files. It seems about as
intuitive to me as what you suggest.

Best regards,

Guillaume