From f97b4b1e33fba9577b8a7a92a5c01b2ca10451f6 Mon Sep 17 00:00:00 2001 From: herbelin Date: Wed, 17 Mar 2004 11:28:04 +0000 Subject: Definition de la notation de la paire par un motif recursif git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5519 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories7/Init/Datatypes.v | 14 ++------------ theories7/Init/Notations.v | 12 ++---------- 2 files changed, 4 insertions(+), 22 deletions(-) (limited to 'theories7') diff --git a/theories7/Init/Datatypes.v b/theories7/Init/Datatypes.v index 508d44ca8..c3758615b 100755 --- a/theories7/Init/Datatypes.v +++ b/theories7/Init/Datatypes.v @@ -78,18 +78,8 @@ 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. - -(* 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. +V7only [Notation "( x , y )" := (pair ? ? x y) : core_scope.]. +V8Notation "( x , y , .. , z )" := (pair ? ? .. (pair ? ? x y) .. z) : core_scope. Section projections. Variables A,B:Set. diff --git a/theories7/Init/Notations.v b/theories7/Init/Notations.v index 2e9e1692d..0cfbdcb64 100644 --- a/theories7/Init/Notations.v +++ b/theories7/Init/Notations.v @@ -58,16 +58,8 @@ Uninterpreted V8Notation "x ^ y" (at level 30, right associativity). (** Notations for pairs *) -Uninterpreted Notation "( x , y )" (at level 0) - 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). +V7only [Uninterpreted Notation "( x , y )" (at level 0) V8only.]. +Uninterpreted V8Notation "( x , y , .. , z )" (at level 0). (** Notation "{ x }" is reserved and has a special status as component of other notations; it is at level 1 to factor with {x:A|P} etc *) -- cgit v1.2.3