changement parametres inductifs dans les theories

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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index 86cd92b85..b538620d1 100755
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -25,10 +25,10 @@ Section Transitive_Closure.
   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.
 
 
@@ -36,11 +36,11 @@ Section Reflexive_Transitive_Closure.
   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.