Remplacement des fichiers .v ancienne syntaxe de theories, contrib et states par les fichiers nouvelle syntaxe

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5027 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 70 insertions, 78 deletions

diff --git a/contrib/correctness/Tuples.v b/contrib/correctness/Tuples.v
index f9a3b56b7..41ff10c04 100644
--- a/contrib/correctness/Tuples.v
+++ b/contrib/correctness/Tuples.v
@@ -12,95 +12,87 @@
 
 (* Tuples *)
 
-Definition tuple_1 := [X:Set]X.
+Definition tuple_1 (X:Set) := X.
 Definition tuple_2 := prod.
 Definition Build_tuple_2 := pair.
 Definition proj_2_1 := fst.
 Definition proj_2_2 := snd.
 
-Record tuple_3 [ T1,T2,T3 : Set ] : Set := 
-  { proj_3_1 : T1 ;
-    proj_3_2 : T2 ;
-    proj_3_3 : T3 }.
-
-Record tuple_4 [ T1,T2,T3,T4 : Set ] : Set := 
-  { proj_4_1 : T1 ;
-    proj_4_2 : T2 ;
-    proj_4_3 : T3 ;
-    proj_4_4 : T4 }.
-
-Record tuple_5 [ T1,T2,T3,T4,T5 : Set ] : Set :=
-  { proj_5_1 : T1 ;
-    proj_5_2 : T2 ;
-    proj_5_3 : T3 ;
-    proj_5_4 : T4 ;
-    proj_5_5 : T5 }.
-
-Record tuple_6 [ T1,T2,T3,T4,T5,T6 : Set ] : Set :=
-  { proj_6_1 : T1 ;
-    proj_6_2 : T2 ;
-    proj_6_3 : T3 ;
-    proj_6_4 : T4 ;
-    proj_6_5 : T5 ;
-    proj_6_6 : T6 }.
-
-Record tuple_7 [ T1,T2,T3,T4,T5,T6,T7 : Set ] : Set :=
-  { proj_7_1 : T1 ;
-    proj_7_2 : T2 ;
-    proj_7_3 : T3 ;
-    proj_7_4 : T4 ;
-    proj_7_5 : T5 ;
-    proj_7_6 : T6 ;
-    proj_7_7 : T7 }.
+Record tuple_3 (T1 T2 T3:Set) : Set := 
+  {proj_3_1 : T1; proj_3_2 : T2; proj_3_3 : T3}.
 
+Record tuple_4 (T1 T2 T3 T4:Set) : Set := 
+  {proj_4_1 : T1; proj_4_2 : T2; proj_4_3 : T3; proj_4_4 : T4}.
 
-(* Existentials *)
-
-Definition sig_1 := sig.
-Definition exist_1 := exist.
-
-Inductive sig_2 [ T1,T2 : Set; P:T1->T2->Prop ] : Set := 
-  exist_2 : (x1:T1)(x2:T2)(P x1 x2) -> (sig_2 T1 T2 P).
-
-Inductive sig_3 [ T1,T2,T3 : Set; P:T1->T2->T3->Prop ] : Set := 
-  exist_3 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3) -> (sig_3 T1 T2 T3 P).
+Record tuple_5 (T1 T2 T3 T4 T5:Set) : Set := 
+  {proj_5_1 : T1; proj_5_2 : T2; proj_5_3 : T3; proj_5_4 : T4; proj_5_5 : T5}.
 
+Record tuple_6 (T1 T2 T3 T4 T5 T6:Set) : Set := 
+  {proj_6_1 : T1;
+   proj_6_2 : T2;
+   proj_6_3 : T3;
+   proj_6_4 : T4;
+   proj_6_5 : T5;
+   proj_6_6 : T6}.
 
-Inductive sig_4 [ T1,T2,T3,T4 : Set;
-                  P:T1->T2->T3->T4->Prop ] : Set :=
-  exist_4 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)
-             (P x1 x2 x3 x4)
-          -> (sig_4 T1 T2 T3 T4 P).
+Record tuple_7 (T1 T2 T3 T4 T5 T6 T7:Set) : Set := 
+  {proj_7_1 : T1;
+   proj_7_2 : T2;
+   proj_7_3 : T3;
+   proj_7_4 : T4;
+   proj_7_5 : T5;
+   proj_7_6 : T6;
+   proj_7_7 : T7}.
 
-Inductive sig_5 [ T1,T2,T3,T4,T5 : Set;
-                  P:T1->T2->T3->T4->T5->Prop ] : Set :=
-  exist_5 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)
-             (P x1 x2 x3 x4 x5)
-          -> (sig_5 T1 T2 T3 T4 T5 P).
 
-Inductive sig_6 [ T1,T2,T3,T4,T5,T6 : Set;
-                  P:T1->T2->T3->T4->T5->T6->Prop ] : Set :=
-  exist_6 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)
-             (P x1 x2 x3 x4 x5 x6)
-          -> (sig_6 T1 T2 T3 T4 T5 T6 P).
-
-Inductive sig_7 [ T1,T2,T3,T4,T5,T6,T7 : Set;
-                  P:T1->T2->T3->T4->T5->T6->T7->Prop ] : Set :=
-  exist_7 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)(x7:T7)
-             (P x1 x2 x3 x4 x5 x6 x7)
-          -> (sig_7 T1 T2 T3 T4 T5 T6 T7 P).
-
-Inductive sig_8 [ T1,T2,T3,T4,T5,T6,T7,T8 : Set;
-                  P:T1->T2->T3->T4->T5->T6->T7->T8->Prop ] : Set :=
-  exist_8 : (x1:T1)(x2:T2)(x3:T3)(x4:T4)(x5:T5)(x6:T6)(x7:T7)(x8:T8)
-             (P x1 x2 x3 x4 x5 x6 x7 x8)
-          -> (sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P).      
-
-Inductive dep_tuple_2 [ T1,T2 : Set; P:T1->T2->Set ] : Set := 
-  Build_dep_tuple_2 : (x1:T1)(x2:T2)(P x1 x2) -> (dep_tuple_2 T1 T2 P).
+(* Existentials *)
 
-Inductive dep_tuple_3 [ T1,T2,T3 : Set; P:T1->T2->T3->Set ] : Set := 
-  Build_dep_tuple_3 : (x1:T1)(x2:T2)(x3:T3)(P x1 x2 x3)
-      	       	   -> (dep_tuple_3 T1 T2 T3 P).
+Definition sig_1 := sig.
+Definition exist_1 := exist.
 
+Inductive sig_2 (T1 T2:Set) (P:T1 -> T2 -> Prop) : Set :=
+    exist_2 : forall (x1:T1) (x2:T2), P x1 x2 -> sig_2 T1 T2 P.
+
+Inductive sig_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Prop) : Set :=
+    exist_3 : forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> sig_3 T1 T2 T3 P.
+
+
+Inductive sig_4 (T1 T2 T3 T4:Set) (P:T1 -> T2 -> T3 -> T4 -> Prop) : Set :=
+    exist_4 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4),
+        P x1 x2 x3 x4 -> sig_4 T1 T2 T3 T4 P.
+
+Inductive sig_5 (T1 T2 T3 T4 T5:Set) (P:T1 -> T2 -> T3 -> T4 -> T5 -> Prop) :
+Set :=
+    exist_5 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5),
+        P x1 x2 x3 x4 x5 -> sig_5 T1 T2 T3 T4 T5 P.
+
+Inductive sig_6 (T1 T2 T3 T4 T5 T6:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> Prop) : Set :=
+    exist_6 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6), P x1 x2 x3 x4 x5 x6 -> sig_6 T1 T2 T3 T4 T5 T6 P.
+
+Inductive sig_7 (T1 T2 T3 T4 T5 T6 T7:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> Prop) : Set :=
+    exist_7 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6) (x7:T7),
+        P x1 x2 x3 x4 x5 x6 x7 -> sig_7 T1 T2 T3 T4 T5 T6 T7 P.
+
+Inductive sig_8 (T1 T2 T3 T4 T5 T6 T7 T8:Set)
+(P:T1 -> T2 -> T3 -> T4 -> T5 -> T6 -> T7 -> T8 -> Prop) : Set :=
+    exist_8 :
+      forall (x1:T1) (x2:T2) (x3:T3) (x4:T4) (x5:T5) 
+        (x6:T6) (x7:T7) (x8:T8),
+        P x1 x2 x3 x4 x5 x6 x7 x8 -> sig_8 T1 T2 T3 T4 T5 T6 T7 T8 P.      
+
+Inductive dep_tuple_2 (T1 T2:Set) (P:T1 -> T2 -> Set) : Set :=
+    Build_dep_tuple_2 :
+      forall (x1:T1) (x2:T2), P x1 x2 -> dep_tuple_2 T1 T2 P.
+
+Inductive dep_tuple_3 (T1 T2 T3:Set) (P:T1 -> T2 -> T3 -> Set) : Set :=
+    Build_dep_tuple_3 :
+      forall (x1:T1) (x2:T2) (x3:T3), P x1 x2 x3 -> dep_tuple_3 T1 T2 T3 P.