The Coq mailing list

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

  Hi,

> I'd like to construct pairs, associated to the right. The following
> recursive notation works, but if I change the ";" symbols into "," I will
> get error messages.
> 
> Notation "{| x , .. , y ; z |}" := (pair x ..(pair y z)..).
> Check ({|1,2,3;4|}).

  Coq grammar extensibility relies on Camlp4 which is (basically) a
parser for LL1 grammars. The notation you wish needs a compilation
of the entry

term ::= rec_pair , subterm
rec_pair ::= subterm , rec_pair
           | subterm

into a LL1

term ::= subterm , rec_pair
rec_pair ::= subterm , rec_pair
           | subterm

what Coq does not do.

  In general, Coq is not intended to factorize the rules itself (it is
up to the user to ensure factorization). In this particular case,
we may however consider doing something specific at the Coq level.

  Best regards,

  Hugo Herbelin