I'm confused about Notations in Coq/Gallina. I have turned my problem into a minimal example: Why in the following the last line does not work?
Definition nOp (a b:nat) := a.
Notation "'nOpOpen' a b 'nOpClose'" := (nOp a b).
Definition foo0 := (nOp 1 0).
Definition foo1 := (nOpOpen 1 0 nOpClose).
//this last line gives
//Syntax error: [term level 200] expected after [term level 200] (in [term]).