diff options
Diffstat (limited to 'theories/Init/DatatypesSyntax.v')
| -rw-r--r-- | theories/Init/DatatypesSyntax.v | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/theories/Init/DatatypesSyntax.v b/theories/Init/DatatypesSyntax.v index 06f28b503..0ba1a5884 100644 --- a/theories/Init/DatatypesSyntax.v +++ b/theories/Init/DatatypesSyntax.v @@ -15,10 +15,12 @@ Require Export Datatypes. Arguments Scope sum [type_scope type_scope]. Arguments Scope prod [type_scope type_scope]. -Infix "+" sum (at level 4, left associativity) : type_scope. -Infix "*" prod (at level 3, right associativity) : type_scope. +Infix LEFTA 4 "+" sum : type_scope. +Notation "x * y" := (prod x y) (at level 3, right associativity) : type_scope + V8only (at level 30, left associativity). -Notation "( x , y )" := (pair ? ? x y) (at level 0). +Notation "( x , y )" := (pair ? ? x y) (at level 0) + V8only "x , y" (at level 150, left associativity). Notation Fst := (fst ? ?). Notation Snd := (snd ? ?). @@ -26,7 +28,8 @@ Arguments Scope option [ type_scope ]. (** Parsing only of things in [Datatypes.v] *) +V7only[ Notation "< A , B > ( x , y )" := (pair A B x y) (at level 1, only parsing, A annot). Notation "< A , B > 'Fst' ( p )" := (fst A B p) (at level 1, only parsing, A annot). Notation "< A , B > 'Snd' ( p )" := (snd A B p) (at level 1, only parsing, A annot). - +]. |