The Coq mailing list

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

  Bonjour Eduardo,

> Notation "'function' n b '=>' e" := 
>  (fun r => match r with (BR n b) => e end) (at level 200). 
> 
> Check (function n b => b).
> > Syntax error: [constr:operconstr level 200] expected after 
> > [constr:operconstr level 200] (in [constr:binder_constr])

  The default is to parse n and b at level 200 (do "Print Grammar
constr" for a confirmation). You have to tell explicitly that they are
identifiers.

Notation "'function' n b '=>' e" := 
 (fun r => match r with (BR n b) => e end) (at level 200, b ident, n ident). 

will work.

  Hugo