diff options
author | 2003-12-16 15:03:50 +0000 | |
---|---|---|
committer | 2003-12-16 15:03:50 +0000 | |
commit | 7b207245cdfd7d91863441ef8e3fa4b99e830fac (patch) | |
tree | 021ca8bb716002b55c7cbe7ef15f9f6ed493056a /theories7 | |
parent | 5eb8860b4326c61e92050a2accebf489d2ebf048 (diff) |
Duplication temporaire des règles de syntaxe des paires
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories7')
-rwxr-xr-x | theories7/Init/Datatypes.v | 13 | ||||
-rw-r--r-- | theories7/Init/Notations.v | 10 | ||||
-rw-r--r-- | theories7/ZArith/Znumtheory.v | 2 |
3 files changed, 22 insertions, 3 deletions
diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v index d93bbbac1..508d44ca8 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 fffdc5200..3cdb8e6ce 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 481639510..300ac520a 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*) |