Passage de Set à Type dans Relations et Wellfounded

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

4 files changed, 16 insertions, 16 deletions

diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index 69421255d..4d6d66c3d 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -18,7 +18,7 @@ Require Import Relation_Operators.
 Require Import Transitive_Closure.
 
 Section Wf_Lexicographic_Exponentiation.
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : A -> A -> Prop.
   
   Notation Power := (Pow A leA).
diff --git a/theories/Wellfounded/Lexicographic_Product.v b/theories/Wellfounded/Lexicographic_Product.v
index 82bede919..f41b6e93d 100644
--- a/theories/Wellfounded/Lexicographic_Product.v
+++ b/theories/Wellfounded/Lexicographic_Product.v
@@ -18,8 +18,8 @@ Require Import Transitive_Closure.
      L. Paulson  JSC (1986) 2, 325-355 *)
 
 Section WfLexicographic_Product.
-  Variable A : Set.
-  Variable B : A -> Set.
+  Variable A : Type.
+  Variable B : A -> Type.
   Variable leA : A -> A -> Prop.
   Variable leB : forall x:A, B x -> B x -> Prop.
 
@@ -74,8 +74,8 @@ End WfLexicographic_Product.
 
 
 Section Wf_Symmetric_Product.
-  Variable A : Set.
-  Variable B : Set.
+  Variable A : Type.
+  Variable B : Type.
   Variable leA : A -> A -> Prop.
   Variable leB : B -> B -> Prop.
 
@@ -106,7 +106,7 @@ End Wf_Symmetric_Product.
 
 Section Swap.
   
-  Variable A : Set.
+  Variable A : Type.
   Variable R : A -> A -> Prop.
 
   Notation SwapProd := (swapprod A R).
@@ -168,4 +168,4 @@ Section Swap.
     apply Acc_swapprod; auto with sets.
   Qed.
 
-End Swap.
\ No newline at end of file
+End Swap.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 1866c5035..5e33da5ff 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -14,7 +14,7 @@ Require Import Relation_Definitions.
 Require Import Relation_Operators.
 
 Section Wf_Transitive_Closure.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Notation trans_clos := (clos_trans A R).
@@ -44,4 +44,4 @@ Section Wf_Transitive_Closure.
     unfold well_founded in |- *; auto with sets.
   Qed.
 
-End Wf_Transitive_Closure.
\ No newline at end of file
+End Wf_Transitive_Closure.
diff --git a/theories/Wellfounded/Well_Ordering.v b/theories/Wellfounded/Well_Ordering.v
index b1cb63be1..7296897ef 100644
--- a/theories/Wellfounded/Well_Ordering.v
+++ b/theories/Wellfounded/Well_Ordering.v
@@ -15,10 +15,10 @@
 Require Import Eqdep.
 
 Section WellOrdering.
-  Variable A : Set.
-  Variable B : A -> Set. 
+  Variable A : Type.
+  Variable B : A -> Type. 
   
-  Inductive WO : Set :=
+  Inductive WO : Type :=
     sup : forall (a:A) (f:B a -> WO), WO.
 
 
@@ -52,7 +52,7 @@ Section Characterisation_wf_relations.
   (*  in course of development                                          *)
 
 
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : A -> A -> Prop.
 
   Definition B (a:A) := {x : A | leA x a}.
@@ -60,12 +60,12 @@ Section Characterisation_wf_relations.
   Definition wof : well_founded leA -> A -> WO A B.
   Proof.
     intros.
-    apply (well_founded_induction H (fun a:A => WO A B)); auto.
-    intros.
+    apply (well_founded_induction_type H (fun a:A => WO A B)); auto.
+    intros x H1.
     apply (sup A B x).
     unfold B at 1 in |- *.
     destruct 1 as [x0].
     apply (H1 x0); auto.
 Qed.
 
-End Characterisation_wf_relations.
\ No newline at end of file
+End Characterisation_wf_relations.