From 283b030353bee1a0a87cb6b67d492adb5dd31979 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Mon, 12 Feb 2007 10:31:53 +0000
Subject: Autres passages de Set à Type dans Relations et Wellfounded
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9642 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Wellfounded/Disjoint_Union.v | 4 ++--
 theories/Wellfounded/Inclusion.v      | 4 ++--
 theories/Wellfounded/Inverse_Image.v  | 2 +-
 theories/Wellfounded/Union.v          | 4 ++--
 4 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'theories/Wellfounded')

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.
-- 
cgit v1.2.3