The Coq mailing list

[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).

Best regards,

Guillaume