diff options
Diffstat (limited to 'theories/Init')
| -rwxr-xr-x | theories/Init/Datatypes.v | 13 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 10 |
2 files changed, 21 insertions, 2 deletions
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v index 2da0d6c02a..7c199bbf35 100755 --- a/theories/Init/Datatypes.v +++ b/theories/Init/Datatypes.v @@ -77,7 +77,18 @@ Inductive prod (A B:Set) : Set := Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. -Notation "x , y" := (pair x y) : core_scope. +Notation "( x , y )" := (pair x y) : core_scope. + +(* Temporary hack *) +Notation "( x1 , x2 , x3 )" := ((x1,x2),x3) : core_scope. +Notation "( x1 , x2 , x3 , x4 )" := ((x1,x2),x3,x4) : core_scope. +Notation "( x1 , x2 , x3 , x4 , x5 )" := ((x1,x2),x3,x4,x5) : core_scope. +Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" + := ((x1,x2),x3,x4,x5,x6) : core_scope. +Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" + := ((x1,x2),x3,x4,x5,x6,x7) : core_scope. +Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" + := ((x1,x2),x3,x4,x5,x6,x7,x8) : core_scope. Section projections. Variables A B : Set. diff --git a/theories/Init/Notations.v b/theories/Init/Notations.v index 2a1c841656..3568991918 100644 --- a/theories/Init/Notations.v +++ b/theories/Init/Notations.v @@ -51,7 +51,15 @@ Reserved Notation "x ^ y" (at level 30, right associativity). (** Notations for pairs *) -Reserved Notation "x , y" (at level 250, left associativity). +(* Temporary hack *) +Reserved Notation "( x , y )" (at level 0). +Reserved Notation "( x , y , z )" (at level 0). +Reserved Notation "( x1 , x2 , x3 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0). +Reserved Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" (at level 0). (** Notations for sum-types *) |