The Coq mailing list

[Michael Shulman <shulman AT sandiego.edu>]

On Tue, Nov 3, 2015 at 8:45 PM, Clément Pit--Claudel
<clement.pit AT gmail.com>
 wrote:
>     Notation "f ( x )" := (f x) (at level 1, format "f ( x )").
>
>     Definition Linear f := forall x y, f(x + y) = f(x) + f(y).
>     Print Linear.

This does work on its own.  However, it also clobbers Coq's parsing
for ever after.  For instance, once Coq starts seeing "f ( x )" as a
notation, it can't parse any more notations with levels or formats:

Notation "f ( x )" := (f x) (at level 1, format "f ( x )").
Notation "x ++ y" := (plus x y) (at level 80).

(* Syntax error: [constr:operconstr level 200] expected after '(' (in
[constr:operconstr]). *)

Nor can I any longer write f(x,y) in the two-variable case, I have to
write f((x,y)).  And I can't define a new notation for that like

Notation "f ( x , y )" := (f (pair x y)) (at level 1, format "f ( x , y )").

since, as noted above, I can't define any more notations with levels or 
formats.

Mike