From d41159a95f2e1c0d610079d462d77a8c80925ae1 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 6 Feb 2007 19:45:52 +0000
Subject: Passage 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@9598 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Relations/Operators_Properties.v |  6 +++---
 theories/Relations/Relation_Operators.v   | 16 ++++++++--------
 theories/Relations/Relations.v            |  4 ++--
 3 files changed, 13 insertions(+), 13 deletions(-)

(limited to 'theories/Relations')

diff --git a/theories/Relations/Operators_Properties.v b/theories/Relations/Operators_Properties.v
index 3cae9d571..4a6d58ec2 100644
--- a/theories/Relations/Operators_Properties.v
+++ b/theories/Relations/Operators_Properties.v
@@ -18,7 +18,7 @@ Require Import Relation_Operators.
 
 Section Properties.
 
-  Variable A : Set.
+  Variable A : Type.
   Variable R : relation A.
 
   Let incl (R1 R2:relation A) : Prop := forall x y:A, R1 x y -> R2 x y.
@@ -43,7 +43,7 @@ Section Properties.
     Qed.
 
     Lemma clos_refl_trans_ind_left :
-      forall (A:Set) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
+      forall (A:Type) (R:A -> A -> Prop) (M:A) (P:A -> Prop),
 	P M ->
 	(forall P0 N:A, clos_refl_trans A R M P0 -> P P0 -> R P0 N -> P N) ->
 	forall a:A, clos_refl_trans A R M a -> P a.
@@ -95,4 +95,4 @@ Section Properties.
   
   End Clos_Refl_Sym_Trans.
 
-End Properties.
\ No newline at end of file
+End Properties.
diff --git a/theories/Relations/Relation_Operators.v b/theories/Relations/Relation_Operators.v
index e4918d40e..c8ace84c3 100644
--- a/theories/Relations/Relation_Operators.v
+++ b/theories/Relations/Relation_Operators.v
@@ -78,7 +78,7 @@ End Union.
 
 
 Section Disjoint_Union.
-Variables A B : Set.
+Variables A B : Type.
 Variable leA : A -> A -> Prop.
 Variable leB : B -> B -> Prop.
 
@@ -94,8 +94,8 @@ End Disjoint_Union.
 Section Lexicographic_Product.
   (* Lexicographic order on dependent pairs *)
 
-  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.
 
@@ -110,8 +110,8 @@ End Lexicographic_Product.
 
 
 Section Symmetric_Product.
-  Variable A : Set.
-  Variable B : Set.
+  Variable A : Type.
+  Variable B : Type.
   Variable leA : A -> A -> Prop.
   Variable leB : B -> B -> Prop.
 
@@ -125,7 +125,7 @@ End Symmetric_Product.
 
 
 Section Swap.
-  Variable A : Set.
+  Variable A : Type.
   Variable R : A -> A -> Prop.
 
   Inductive swapprod : A * A -> A * A -> Prop :=
@@ -138,7 +138,7 @@ End Swap.
 
 Section Lexicographic_Exponentiation.
   
-  Variable A : Set.
+  Variable A : Type.
   Variable leA : A -> A -> Prop.
   Let Nil := nil (A:=A).
   Let List := list A.
@@ -156,7 +156,7 @@ Section Lexicographic_Exponentiation.
       forall (x y:A) (l:List),
         leA x y -> Desc (l ++ y :: Nil) -> Desc ((l ++ y :: Nil) ++ x :: Nil).
 
-  Definition Pow : Set := sig Desc.
+  Definition Pow : Type := sig Desc.
   
   Definition lex_exp (a b:Pow) : Prop := Ltl (proj1_sig a) (proj1_sig b).
 
diff --git a/theories/Relations/Relations.v b/theories/Relations/Relations.v
index 938d514df..1c6df08a4 100644
--- a/theories/Relations/Relations.v
+++ b/theories/Relations/Relations.v
@@ -13,7 +13,7 @@ Require Export Relation_Operators.
 Require Export Operators_Properties.
 
 Lemma inverse_image_of_equivalence :
-  forall (A B:Set) (f:A -> B) (r:relation B),
+  forall (A B:Type) (f:A -> B) (r:relation B),
     equivalence B r -> equivalence A (fun x y:A => r (f x) (f y)).
 Proof.
   intros; split; elim H; red in |- *; auto.
@@ -21,7 +21,7 @@ Proof.
 Qed.
 
 Lemma inverse_image_of_eq :
-  forall (A B:Set) (f:A -> B), equivalence A (fun x y:A => f x = f y).
+  forall (A B:Type) (f:A -> B), equivalence A (fun x y:A => f x = f y).
 Proof.
   split; red in |- *;
     [  (* reflexivity *) reflexivity
-- 
cgit v1.2.3