migration from Set to Type of FSet/FMap + some dependencies...

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

1 files changed, 4 insertions, 4 deletions

diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index 20dc61ef1..77caa9c22 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -20,7 +20,7 @@ Set Implicit Arguments.
 
 Section first_definitions.
 
-  Variable A : Set.
+  Variable A : Type.
   Hypothesis Aeq_dec : forall x y:A, {x = y} + {x <> y}.
 
   Definition set := list A.
@@ -100,7 +100,7 @@ Section first_definitions.
   Qed.
 
   Lemma set_mem_ind :
-   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
      (set_In a x -> P y) -> P z -> P (if set_mem a x then y else z).
 
   Proof.
@@ -110,7 +110,7 @@ Section first_definitions.
   Qed.
 
   Lemma set_mem_ind2 :
-   forall (B:Set) (P:B -> Prop) (y z:B) (a:A) (x:set),
+   forall (B:Type) (P:B -> Prop) (y z:B) (a:A) (x:set),
      (set_In a x -> P y) ->
      (~ set_In a x -> P z) -> P (if set_mem a x then y else z).
 
@@ -373,7 +373,7 @@ End first_definitions.
 
 Section other_definitions.
 
-  Variables A B : Set.
+  Variables A B : Type.
 
   Definition set_prod : set A -> set B -> set (A * B) :=
     list_prod (A:=A) (B:=B).