The Coq mailing list

[roconnor AT theorem.ca]

On Tue, 17 Oct 2006, Hugo Herbelin wrote:

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

Thanks.  Would it be reasonable to disallow notations that conflict with 
the normal Coq language, or is it not worth it because there is a more 
general problem of notations from different developments conflicting with 
each other?

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''