changement parametres inductifs dans les theories

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

5 files changed, 29 insertions, 30 deletions

diff --git a/theories/Init/Wf.v b/theories/Init/Wf.v
index 584e68657..5a05f7b65 100755
--- a/theories/Init/Wf.v
+++ b/theories/Init/Wf.v
@@ -29,8 +29,8 @@ Section Well_founded.
 
  (** The accessibility predicate is defined to be non-informative *)
 
- Inductive Acc : A -> Prop :=
-     Acc_intro : forall x:A, (forall y:A, R y x -> Acc y) -> Acc x.
+ Inductive Acc (x: A) : Prop :=
+     Acc_intro : (forall y:A, R y x -> Acc y) -> Acc x.
 
  Lemma Acc_inv : forall x:A, Acc x -> forall y:A, R y x -> Acc y.
   destruct 1; trivial.
diff --git a/theories/Lists/Streams.v b/theories/Lists/Streams.v
index f69041eb8..366172381 100755
--- a/theories/Lists/Streams.v
+++ b/theories/Lists/Streams.v
@@ -71,9 +71,8 @@ Qed.
 
 (** Extensional Equality between two streams  *)
 
-CoInductive EqSt : Stream -> Stream -> Prop :=
+CoInductive EqSt (s1 s2: Stream) : Prop :=
     eqst :
-      forall s1 s2:Stream,
         hd s1 = hd s2 -> EqSt (tl s1) (tl s2) -> EqSt s1 s2.
 
 (** A coinduction principle *)
@@ -140,12 +139,12 @@ Inductive Exists : Stream -> Prop :=
   | Further : forall x:Stream, ~ P x -> Exists (tl x) -> Exists x.
 i*)
 
-Inductive Exists : Stream -> Prop :=
-  | Here : forall x:Stream, P x -> Exists x
-  | Further : forall x:Stream, Exists (tl x) -> Exists x.
+Inductive Exists ( x: Stream ) : Prop :=
+  | Here : P x -> Exists x
+  | Further : Exists (tl x) -> Exists x.
 
-CoInductive ForAll : Stream -> Prop :=
-    HereAndFurther : forall x:Stream, P x -> ForAll (tl x) -> ForAll x.
+CoInductive ForAll (x: Stream) : Prop :=
+    HereAndFurther : P x -> ForAll (tl x) -> ForAll x.
 
 
 Section Co_Induction_ForAll.
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.
 
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).
diff --git a/theories/Sets/Relations_3.v b/theories/Sets/Relations_3.v
index d6202cffe..ec8fb7e6d 100755
--- a/theories/Sets/Relations_3.v
+++ b/theories/Sets/Relations_3.v
@@ -46,9 +46,9 @@ Section Relations_3.
    
    Definition Confluent : Prop := forall x:U, confluent x.
    
-   Inductive noetherian : U -> Prop :=
+   Inductive noetherian (x: U) : Prop :=
        definition_of_noetherian :
-         forall x:U, (forall y:U, R x y -> noetherian y) -> noetherian x.
+         (forall y:U, R x y -> noetherian y) -> noetherian x.
    
    Definition Noetherian : Prop := forall x:U, noetherian x.