The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi,

> Is it the case that if one declares a notation for ; that records become 
> impossible to declare, even if the scope is closed?

  Coq has a unique global parser, that does not care about whether
scopes are open or closed. So, when a notation with a syntax that it
is not already reserved is declared, it extends the global parser with
a new parsing rule that becomes active independently of which scopes
are open or closed. The scopes are only used to decide how to
interpret a phrase recognized by the parser, not to parse it.

  Moreover, having a notation accepted does not ensure by any means
that the added parsing rule does not conflict with other rules of the
grammar. For instance, if you add a notation of the form "x ; y", what
you probably did, it definitively hides the parsing rule for record
fields. Coq is constrained with the LL constraints of its underlying
extensible parsing tool Camlp4.

  Note that the global parser can be displayed using the commands
"Print Grammar constr", "Print Grammar tactic" and "Print Grammar
vernac". As an example, a notation like "( x ; y )", at level 0,
shouldn't create conflicts.

  Hugo Herbelin