Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

6 files changed, 19 insertions, 19 deletions

diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v
index 3cf604d8..ae914933 100755..100644
--- a/theories/Relations/Newman.v
+++ b/theories/Relations/Newman.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Newman.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Newman.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Import Rstar.
 
diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 5e0e9ec8..22a08a27 100755..100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Operators_Properties.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Operators_Properties.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (****************************************************************************)
 (*                            Bruno Barras                                  *)
diff --git a/theories/Relations/Relation_Definitions.v b/theories/Relations/Relation_Definitions.v
index e115b0b0..22ba7413 100755..100644
--- a/theories/Relations/Relation_Definitions.v
+++ b/theories/Relations/Relation_Definitions.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relation_Definitions.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relation_Definitions.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Section Relation_Definition.
 
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index b6359ada..edc112e5 100755..100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relation_Operators.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relation_Operators.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (****************************************************************************)
 (*                      Bruno Barras, Cristina Cornes                       *)
@@ -22,31 +22,31 @@ Require Import List.
 (** Some operators to build relations *)
 
 Section Transitive_Closure.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
-  Inductive clos_trans : A -> A -> Prop :=
-    | t_step : forall x y:A, R x y -> clos_trans x y
+  Inductive clos_trans (x: A) : A -> Prop :=
+    | t_step : forall y:A, R x y -> clos_trans x y
     | t_trans :
-        forall x y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
+        forall y z:A, clos_trans x y -> clos_trans y z -> clos_trans x z.
 End Transitive_Closure.
 
 
 Section Reflexive_Transitive_Closure.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
-  Inductive clos_refl_trans : relation A :=
-    | rt_step : forall x y:A, R x y -> clos_refl_trans x y
-    | rt_refl : forall x:A, clos_refl_trans x x
+  Inductive clos_refl_trans (x:A) : A -> Prop:=
+    | rt_step : forall y:A, R x y -> clos_refl_trans x y
+    | rt_refl : clos_refl_trans x x
     | rt_trans :
-        forall x y z:A,
+        forall y z:A,
           clos_refl_trans x y -> clos_refl_trans y z -> clos_refl_trans x z.
 End Reflexive_Transitive_Closure.
 
 
 Section Reflexive_Symetric_Transitive_Closure.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Inductive clos_refl_sym_trans : relation A :=
@@ -62,7 +62,7 @@ End Reflexive_Symetric_Transitive_Closure.
 
 
 Section Transposee.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Definition transp (x y:A) := R y x.
@@ -70,7 +70,7 @@ End Transposee.
 
 
 Section Union.
-  Variable A : Set.
+  Variable A : Type.
   Variables R1 R2 : relation A.
 
   Definition union (x y:A) := R1 x y \/ R2 x y.
@@ -164,4 +164,4 @@ End Lexicographic_Exponentiation.
 
 Hint Unfold transp union: sets v62.
 Hint Resolve t_step rt_step rt_refl rst_step rst_refl: sets v62.
-Hint Immediate rst_sym: sets v62.
\ No newline at end of file
+Hint Immediate rst_sym: sets v62.
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 6c96f14d..2df0317b 100755..100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Relations.v,v 1.6.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Relations.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 Require Export Relation_Definitions.
 Require Export Relation_Operators.
diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v
index 7bb3ee93..4e62d73a 100755..100644
--- a/theories/Relations/Rstar.v
+++ b/theories/Relations/Rstar.v
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Rstar.v,v 1.8.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
+(*i $Id: Rstar.v 8642 2006-03-17 10:09:02Z notin $ i*)
 
 (** Properties of a binary relation [R] on type [A] *)