diff options
| -rwxr-xr-x | theories/Init/Datatypes.v | 13 | ||||
| -rw-r--r-- | theories/Init/Notations.v | 10 | ||||
| -rw-r--r-- | theories/ZArith/Znumtheory.v | 3 | ||||
| -rwxr-xr-x | theories7/Init/Datatypes.v | 13 | ||||
| -rw-r--r-- | theories7/Init/Notations.v | 10 | ||||
| -rw-r--r-- | theories7/ZArith/Znumtheory.v | 2 |
6 files changed, 44 insertions, 7 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 *) diff --git a/theories/ZArith/Znumtheory.v b/theories/ZArith/Znumtheory.v index 8bd5117dcc..46ba76ffc7 100644 --- a/theories/ZArith/Znumtheory.v +++ b/theories/ZArith/Znumtheory.v @@ -30,8 +30,7 @@ Inductive Zdivide (a b:Z) : Prop := (** Syntax for divisibility *) -Notation "a | b" := (Zdivide a b) (at level 260, no associativity) : - Z_scope. +Notation "( a | b )" := (Zdivide a b) (at level 0) : Z_scope. (** Results concerning divisibility*) diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v index d93bbbac16..508d44ca87 100755 --- a/theories7/Init/Datatypes.v +++ b/theories7/Init/Datatypes.v @@ -78,7 +78,18 @@ Inductive prod [A,B:Set] : Set := pair : A -> B -> (prod A B). Add Printing Let prod. Notation "x * y" := (prod x y) : type_scope. -Notation "( x , y )" := (pair ? ? x y) : core_scope V8only "x , y". +Notation "( x , y )" := (pair ? ? x y) : core_scope V8only. + +(* Temporary hack *) +V8Notation "( x1 , x2 , x3 )" := ((x1,x2),x3) : core_scope. +V8Notation "( x1 , x2 , x3 , x4 )" := (((x1,x2),x3),x4) : core_scope. +V8Notation "( x1 , x2 , x3 , x4 , x5 )" := ((((x1,x2),x3),x4),x5) : core_scope. +V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" + := (((((x1,x2),x3),x4),x5),x6) : core_scope. +V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" + := ((((((x1,x2),x3),x4),x5),x6),x7) : core_scope. +V8Notation "( 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/theories7/Init/Notations.v b/theories7/Init/Notations.v index fffdc52004..3cdb8e6ce4 100644 --- a/theories7/Init/Notations.v +++ b/theories7/Init/Notations.v @@ -59,7 +59,15 @@ Uninterpreted V8Notation "x ^ y" (at level 30, right associativity). (** Notations for pairs *) Uninterpreted Notation "( x , y )" (at level 0) - V8only "x , y" (at level 250, left associativity). + V8only "( x , y )" (at level 0). + +Uninterpreted V8Notation "( x1 , x2 , x3 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 , x4 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 )" (at level 0). +Uninterpreted V8Notation "( x1 , x2 , x3 , x4 , x5 , x6 , x7 , x8 )" (at level 0). (** Notations for sum-types *) diff --git a/theories7/ZArith/Znumtheory.v b/theories7/ZArith/Znumtheory.v index 4816395108..300ac520a0 100644 --- a/theories7/ZArith/Znumtheory.v +++ b/theories7/ZArith/Znumtheory.v @@ -33,7 +33,7 @@ Inductive Zdivide [a,b:Z] : Prop := Notation "( a | b )" := (Zdivide a b) (at level 0, a,b at level 10) : Z_scope - V8only "a | b" (at level 260, no associativity). + V8only "( a | b )" (at level 0). (** Results concerning divisibility*) |