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, 12 insertions, 12 deletions

diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v
index 918e45ee1..11ac85e84 100755
--- a/theories/Sets/Relations_2.v
+++ b/theories/Sets/Relations_2.v
@@ -32,18 +32,18 @@ Section Relations_2.
 Variable U : Type.
 Variable R : Relation U.
 
-Inductive Rstar : Relation U :=
-  | Rstar_0 : forall x:U, Rstar x x
-  | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z.
-
-Inductive Rstar1 : Relation U :=
-  | Rstar1_0 : forall x:U, Rstar1 x x
-  | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y
-  | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
-
-Inductive Rplus : Relation U :=
-  | Rplus_0 : forall x y:U, R x y -> Rplus x y
-  | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z.
+Inductive Rstar (x:U) : U -> Prop :=
+  | Rstar_0 : Rstar x x
+  | Rstar_n : forall y z:U, R x y -> Rstar y z -> Rstar x z.
+
+Inductive Rstar1 (x:U) : U -> Prop :=
+  | Rstar1_0 : Rstar1 x x
+  | Rstar1_1 : forall y:U, R x y -> Rstar1 x y
+  | Rstar1_n : forall y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z.
+
+Inductive Rplus (x:U) : U -> Prop :=
+  | Rplus_0 : forall y:U, R x y -> Rplus x y
+  | Rplus_n : forall y z:U, R x y -> Rplus y z -> Rplus x z.
 
 Definition Strongly_confluent : Prop :=
   forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z).