The Coq mailing list

[CJ Bell <cbell AT CS.Princeton.EDU>]

On Fri, May 17, 2013 at 12:52 PM, Jason Gross 
<jasongross9 AT gmail.com>
 wrote:
> Is there a reason that files don't pack notations into scopes specific to
> the development, and then have one module which can be imported for
> notations which just opens the appropriate scopes and binds the appropriate
> scopes to the appropriate types?


Because defining, or even reserving, a notation changes the parsing
behavior regardless of whether the scope is opened or not. If the
notation is defined within a module, then it does not change the
parsing behavior until the module is imported.

For example:

Notation "a ; b" := (plus a b) (at level 50) : my_scope.
(* Records can no longer be parsed, even though my_scope has not been opened! 
*)
Record a := {aa:nat; bb:nat}.

In comparison:

Module A.
  Notation "a ; b" := (plus a b) (at level 50) : my_scope.
End A.
(* Not broken *)
Record a := {aa:nat; bb:nat}.
Import A.
(* Broken *)
Record b := {cc:nat; dd:nat}.


Defining a notation for ";" is a little contrived because it should
*never* be done, but there are many other ways to define notations
that conflict with each other in this way (even when their scopes are
not open).

-cj