The Coq mailing list

[Jason Gross <jasongross9 AT gmail.com>]

Can someone explain to me what is happening in the following code (in particular, in the last line)?  Is this a bug?

Parameter foo : Type -> Type -> Type -> Type.

Parameter bar : Type -> Type -> Type.

(* Notation "C ~ D" := (bar C D). (* Error: A left-recursive notation must have an explicit level. *) *)

(* Notation "C .^{ M } D" := (foo C M D). (* Error: A left-recursive notation must have an explicit level. *) *)

Reserved Notation "C .^{ M } D" (at level 70, no associativity).

Reserved Notation "C ~ D" (at level 70, no associativity).

Notation "C ~ D" := (bar C D). (* works fine *)

(* Notation "C .^{ M } D" := (foo C M D) (at level 70, no associativity). (* would work fine *) *)

Notation "C .^{ M } D" := (foo C M D). (* Error: A left-recursive notation must have an explicit level. *)

Thanks.

-Jason