4 files changed, 7 insertions, 7 deletions
diff --git a/theories/Wellfounded/Disjoint_Union.v b/theories/Wellfounded/Disjoint_Union.v
index c82549e37..f6ce84f98 100644
--- a/theories/Wellfounded/Disjoint_Union.v
+++ b/theories/Wellfounded/Disjoint_Union.v
@@ -15,7 +15,7 @@
 Require Import Relation_Operators.
 
 Section Wf_Disjoint_Union.
-  Variables A B : Set.
+  Variables A B : Type.
   Variable leA : A -> A -> Prop.
   Variable leB : B -> B -> Prop.
 
@@ -52,4 +52,4 @@ Section Wf_Disjoint_Union.
     apply (H0 b).
   Qed.
 
-End Wf_Disjoint_Union.
-\ No newline at end of file
+End Wf_Disjoint_Union.
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index 7c69b6765..e72b1e11d 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -13,7 +13,7 @@
 Require Import Relation_Definitions.
 
 Section WfInclusion.
-  Variable A : Set.
+  Variable A : Type.
   Variables R1 R2 : A -> A -> Prop.
 
   Lemma Acc_incl : inclusion A R1 R2 -> forall z:A, Acc R2 z -> Acc R1 z.
@@ -29,4 +29,4 @@ Section WfInclusion.
     unfold well_founded in |- *; auto with sets.
   Qed.
 
-End WfInclusion.
-\ No newline at end of file
+End WfInclusion.
diff --git a/theories/Wellfounded/Inverse_Image.v b/theories/Wellfounded/Inverse_Image.v
index 94ca69538..df6a61198 100644
--- a/theories/Wellfounded/Inverse_Image.v
+++ b/theories/Wellfounded/Inverse_Image.v
@@ -12,7 +12,7 @@
 
 Section Inverse_Image.
 
-  Variables A B : Set.
+  Variables A B : Type.
   Variable R : B -> B -> Prop.
   Variable f : A -> B.
 
diff --git a/theories/Wellfounded/Union.v b/theories/Wellfounded/Union.v
index da1b78caa..ebf4ba98e 100644
--- a/theories/Wellfounded/Union.v
+++ b/theories/Wellfounded/Union.v
@@ -15,7 +15,7 @@ Require Import Relation_Definitions.
 Require Import Transitive_Closure.
 
 Section WfUnion.
-  Variable A : Set.
+  Variable A : Type.
   Variables R1 R2 : relation A.
   
   Notation Union := (union A R1 R2).
@@ -72,4 +72,4 @@ Section WfUnion.
     apply Acc_union; auto with sets.
   Qed.
 
-End WfUnion.
-\ No newline at end of file
+End WfUnion.