As suggested by Pierre Casteran, fold for FSets/FMaps now takes a

(A:Type) instead of a (A:Set). 



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

14 files changed, 51 insertions, 51 deletions

diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index 3cd6274cca..cc2d04e58c 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -1073,17 +1073,17 @@ Hint Resolve elements_sort.
 
 (** * Fold *)
 
-Fixpoint fold (A : Set) (f : key -> elt -> A -> A)(s : t elt) {struct s} : A -> A := 
+Fixpoint fold (A : Type) (f : key -> elt -> A -> A)(s : t elt) {struct s} : A -> A := 
  fun a => match s with
   | Leaf => a
   | Node l x e r _ => fold f r (f x e (fold f l a))
  end.
 
-Definition fold' (A : Set) (f : key -> elt -> A -> A)(s : t elt) := 
+Definition fold' (A : Type) (f : key -> elt -> A -> A)(s : t elt) := 
   L.fold f (elements s).
 
 Lemma fold_equiv_aux :
- forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc,
+ forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A) acc,
  L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
 Proof.
  simple induction s.
@@ -1095,7 +1095,7 @@ Proof.
 Qed.
 
 Lemma fold_equiv :
- forall (A : Set) (s : t elt) (f : key -> elt -> A -> A) (a : A),
+ forall (A : Type) (s : t elt) (f : key -> elt -> A -> A) (a : A),
  fold f s a = fold' f s a.
 Proof.
  unfold fold', elements in |- *. 
@@ -1106,7 +1106,7 @@ Proof.
 Qed.
 
 Lemma fold_1 : 
- forall (s:t elt)(Hs:bst s)(A : Set)(i:A)(f : key -> elt -> A -> A),
+ forall (s:t elt)(Hs:bst s)(A : Type)(i:A)(f : key -> elt -> A -> A),
  fold f s i = fold_left (fun a p => f (fst p) (snd p) a) (elements s) i.
 Proof.
  intros.
@@ -1739,7 +1739,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Definition map2 f m (m':t elt') : t elt'' := 
   Bbst (Raw.map2_bst f m m') (Raw.map2_avl f m m').
  Definition elements m : list (key*elt) := Raw.elements m.(this).
- Definition fold (A:Set) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i.
+ Definition fold (A:Type) (f:key->elt->A->A) m i := Raw.fold (A:=A) f m.(this) i.
  Definition equal cmp m m' : bool := 
    if (Raw.equal cmp m.(is_bst) m'.(is_bst)) then true else false.
 
@@ -1797,7 +1797,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Lemma find_2 : forall m x e, find x m = Some e -> MapsTo x e m.
  Proof. intros m; exact (@Raw.find_2 elt m.(this)). Qed.
 
- Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A),
+ Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this) m.(is_bst)). Qed.
 
diff --git a/theories/FSets/FMapIntMap.v b/theories/FSets/FMapIntMap.v
index 90df4019f4..6ad24f1cc5 100644
--- a/theories/FSets/FMapIntMap.v
+++ b/theories/FSets/FMapIntMap.v
@@ -320,11 +320,11 @@ Module MapIntMap <: S with Module E:=NUsualOrderedType.
   (** unfortunately, the [MapFold] of [IntMap] isn't compatible with 
    the FMap interface. We use a naive version for now : *)
 
-  Definition fold (B:Set)(f:key -> A -> B -> B)(m:t A)(i:B) : B := 
+  Definition fold (B:Type)(f:key -> A -> B -> B)(m:t A)(i:B) : B := 
     fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 
   Lemma fold_1 :
-	forall (B:Set) (i : B) (f : key -> A -> B -> B),
+	forall (B:Type) (i : B) (f : key -> A -> B -> B),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
   Proof. auto. Qed.
 
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index e5c9e59eec..03c64b1efc 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -99,7 +99,7 @@ Module Type S.
          Elements of this list are sorted with respect to their first components. 
          Useful to specify [fold] ... *)
 
-    Parameter fold : forall A: Set, (key -> elt -> A -> A) -> t elt -> A -> A.
+    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
     (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
 	where [k1] ... [kN] are the keys of all bindings in [m] 
 	(in increasing order), and [d1] ... [dN] are the associated data. *)
@@ -166,7 +166,7 @@ Module Type S.
 
     (** Specification of [fold] *)  
       Parameter fold_1 :
-	forall (A : Set) (i : A) (f : key -> elt -> A -> A),
+	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  
    Definition Equal cmp m m' := 
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 86f1dfdc20..60a48396dc 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -349,13 +349,13 @@ Qed.
 
 (** * [fold] *)
 
-Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} :  A :=
+Function fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc:A) {struct m} :  A :=
   match m with
    | nil => acc
    | (k,e)::m' => fold f m' (f k e acc)
   end.
 
-Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A),
+Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A),
   fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 Proof. 
  intros; functional induction (fold f m i); auto.
@@ -1060,7 +1060,7 @@ Section Elt.
  Definition map2 f m (m':t elt') : t elt'' := 
    Build_slist (Raw.map2_sorted f m.(sorted) m'.(sorted)).
  Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
- Definition fold (A:Set)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
+ Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
 
  Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
@@ -1114,7 +1114,7 @@ Section Elt.
  Lemma elements_3 : forall m, sort lt_key (elements m).  
  Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(sorted)). Qed.
 
- Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A),
+ Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
 
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v
index af1e71de5d..c3bdc773b2 100644
--- a/theories/FSets/FMapPositive.v
+++ b/theories/FSets/FMapPositive.v
@@ -957,11 +957,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits.
   Qed.
 
 
-  Definition fold (A B : Set) (f: positive -> A -> B -> B) (tr: t A) (v: B) :=
+  Definition fold (A : Set)(B : Type) (f: positive -> A -> B -> B) (tr: t A) (v: B) :=
      List.fold_left (fun a p => f (fst p) (snd p) a) (elements tr) v.
   
   Lemma fold_1 :
-    forall (A:Set)(m:t A)(B:Set)(i : B) (f : key -> A -> B -> B),
+    forall (A:Set)(m:t A)(B:Type)(i : B) (f : key -> A -> B -> B),
     fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
   Proof.
   intros; unfold fold; auto.
diff --git a/theories/FSets/FMapWeakInterface.v b/theories/FSets/FMapWeakInterface.v
index ddcd2f43f5..c5f5fd7df6 100644
--- a/theories/FSets/FMapWeakInterface.v
+++ b/theories/FSets/FMapWeakInterface.v
@@ -89,7 +89,7 @@ Module Type S.
          Elements of this list are sorted with respect to their first components. 
          Useful to specify [fold] ... *)
 
-    Parameter fold : forall A: Set, (key -> elt -> A -> A) -> t elt -> A -> A.
+    Parameter fold : forall A: Type, (key -> elt -> A -> A) -> t elt -> A -> A.
     (** [fold f m a] computes [(f kN dN ... (f k1 d1 a)...)], 
 	where [k1] ... [kN] are the keys of all bindings in [m] 
 	(in increasing order), and [d1] ... [dN] are the associated data. *)
@@ -154,7 +154,7 @@ Module Type S.
 
     (** Specification of [fold] *)  
       Parameter fold_1 :
-	forall (A : Set) (i : A) (f : key -> elt -> A -> A),
+	forall (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  
    Definition Equal cmp m m' := 
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 7a1987fe7a..76d2b9c3bc 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -347,13 +347,13 @@ Qed.
 
 (** * [fold] *)
 
-Function fold (A:Set)(f:key->elt->A->A)(m:t elt) (acc : A) {struct m} :  A :=
+Function fold (A:Type)(f:key->elt->A->A)(m:t elt) (acc : A) {struct m} :  A :=
   match m with
    | nil => acc
    | (k,e)::m' => fold f m' (f k e acc)
   end.
 
-Lemma fold_1 : forall m (A:Set)(i:A)(f:key->elt->A->A),
+Lemma fold_1 : forall m (A:Type)(i:A)(f:key->elt->A->A),
   fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
 Proof. 
  intros; functional induction (@fold A f m i); auto.
@@ -901,7 +901,7 @@ Section Elt.
  Definition map2 f m (m':t elt') : t elt'' := 
    Build_slist (Raw.map2_NoDup f m.(NoDup) m'.(NoDup)).
  Definition elements m : list (key*elt) := @Raw.elements elt m.(this).
- Definition fold (A:Set)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
+ Definition fold (A:Type)(f:key->elt->A->A) m (i:A) : A := @Raw.fold elt A f m.(this) i.
  Definition equal cmp m m' : bool := @Raw.equal elt cmp m.(this) m'.(this).
 
  Definition MapsTo x e m : Prop := Raw.PX.MapsTo x e m.(this).
@@ -954,7 +954,7 @@ Section Elt.
  Lemma elements_3 : forall m, NoDupA eq_key (elements m).  
  Proof. intros m; exact (@Raw.elements_3 elt m.(this) m.(NoDup)). Qed.
 
- Lemma fold_1 : forall m (A : Set) (i : A) (f : key -> elt -> A -> A),
+ Lemma fold_1 : forall m (A : Type) (i : A) (f : key -> elt -> A -> A),
         fold f m i = fold_left (fun a p => f (fst p) (snd p) a) (elements m) i.
  Proof. intros m; exact (@Raw.fold_1 elt m.(this)). Qed.
 
diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index f21ae6e8ca..f12a92e07c 100644
--- a/theories/FSets/FSetAVL.v
+++ b/theories/FSets/FSetAVL.v
@@ -1706,19 +1706,19 @@ End F.
 
 Module L := FSetList.Raw X.
 
-Fixpoint fold (A : Set) (f : elt -> A -> A)(s : tree) {struct s} : A -> A := 
+Fixpoint fold (A : Type) (f : elt -> A -> A)(s : tree) {struct s} : A -> A := 
  fun a => match s with
   | Leaf => a
   | Node l x r _ => fold A f r (f x (fold A f l a))
  end.
 Implicit Arguments fold [A].
 
-Definition fold' (A : Set) (f : elt -> A -> A)(s : tree) := 
+Definition fold' (A : Type) (f : elt -> A -> A)(s : tree) := 
   L.fold f (elements s).
 Implicit Arguments fold' [A].
 
 Lemma fold_equiv_aux :
- forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt),
+ forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A) (acc : list elt),
  L.fold f (elements_aux acc s) a = L.fold f acc (fold f s a).
 Proof.
  simple induction s.
@@ -1730,7 +1730,7 @@ Proof.
 Qed.
 
 Lemma fold_equiv :
- forall (A : Set) (s : tree) (f : elt -> A -> A) (a : A),
+ forall (A : Type) (s : tree) (f : elt -> A -> A) (a : A),
  fold f s a = fold' f s a.
 Proof.
  unfold fold', elements in |- *. 
@@ -1741,7 +1741,7 @@ Proof.
 Qed.
 
 Lemma fold_1 : 
- forall (s:t)(Hs:bst s)(A : Set)(f : elt -> A -> A)(i : A),
+ forall (s:t)(Hs:bst s)(A : Type)(f : elt -> A -> A)(i : A),
  fold f s i = fold_left (fun a e => f e a) (elements s) i.
 Proof.
  intros.
@@ -2621,7 +2621,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  Definition min_elt (s:t) : option elt := Raw.min_elt s.
  Definition max_elt (s:t) : option elt := Raw.max_elt s.
  Definition choose (s:t) : option elt := Raw.choose s.
- Definition fold (B : Set) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. 
+ Definition fold (B : Type) (f : elt -> B -> B) (s:t) : B -> B := Raw.fold f s. 
  Definition cardinal (s:t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s:t) : t := 
    Bbst _ (Raw.filter_bst f _ (is_bst s) (is_avl s))
@@ -2816,7 +2816,7 @@ Module IntMake (I:Int)(X: OrderedType) <: S with Module E := X.
  unfold diff, In; simpl; rewrite Raw.diff_in; intuition.
  Qed.
  
- Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+ Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold A f s i = fold_left (fun a e => f e a) (elements s) i.
  Proof. 
  unfold fold, elements; intros; apply Raw.fold_1; auto.
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index f517898e14..55b00f063f 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -115,7 +115,7 @@ Module DepOfNodep (M: S) <: Sdep with Module E := M.E.
    Defined. 
 
   Definition fold :
-    forall (A : Set) (f : elt -> A -> A) (s : t) (i : A),
+    forall (A : Type) (f : elt -> A -> A) (s : t) (i : A),
     {r : A |   let (l,_) := elements s in 
                   r = fold_left (fun a e => f e a) l i}.
   Proof. 
@@ -648,11 +648,11 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
     destruct (M.elements s); auto.
   Qed.
 
-  Definition fold (B : Set) (f : elt -> B -> B) (i : t) 
+  Definition fold (B : Type) (f : elt -> B -> B) (i : t) 
     (s : B) : B := let (fold, _) := fold f i s in fold.
 
   Lemma fold_1 :
-   forall (s : t) (A : Set) (i : A) (f : elt -> A -> A),
+   forall (s : t) (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
     intros; unfold fold in |- *; case (M.fold f s i); unfold elements in *; 
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 50e6fb5395..6f23907b36 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -20,11 +20,11 @@ Unset Strict Implicit.
 (* end hide *)
 
 (** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
+Definition compat_bool (A:Type)(eqA: A->A->Prop)(f: A-> bool) :=
   forall x y : A, eqA x y -> f x = f y.
 
 (** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) :=
+Definition compat_P (A:Type)(eqA: A->A->Prop)(P : A -> Prop) :=
   forall x y : A, eqA x y -> P x -> P y.
 
 Hint Unfold compat_bool compat_P.
@@ -101,7 +101,7 @@ Module Type S.
   The order in which the elements of [s] are presented to [f]
   is unspecified. *)
 
-  Parameter fold : forall A : Set, (elt -> A -> A) -> t -> A -> A.
+  Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.
   (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
   where [x1 ... xN] are the elements of [s], in increasing order. *)
 
@@ -216,7 +216,7 @@ Module Type S.
   Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
  
   (** Specification of [fold] *)  
-  Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+  Parameter fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
 
   (** Specification of [cardinal] *)  
@@ -401,7 +401,7 @@ Module Type Sdep.
 
   Parameter
     fold :
-      forall (A : Set) (f : elt -> A -> A) (s : t) (i : A),
+      forall (A : Type) (f : elt -> A -> A) (s : t) (i : A),
       {r : A | let (l,_) := elements s in 
                   r = fold_left (fun a e => f e a) l i}.
 
diff --git a/theories/FSets/FSetList.v b/theories/FSets/FSetList.v
index a9f81008d2..dd7effdb80 100644
--- a/theories/FSets/FSetList.v
+++ b/theories/FSets/FSetList.v
@@ -145,7 +145,7 @@ Module Raw (X: OrderedType).
     | _, _ => false
     end.
 
-  Fixpoint fold (B : Set) (f : elt -> B -> B) (s : t) {struct s} : 
+  Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} : 
    B -> B := fun i => match s with
                       | nil => i
                       | x :: l => fold f l (f x i)
@@ -750,7 +750,7 @@ Module Raw (X: OrderedType).
   Qed.   
    
   Lemma fold_1 :
-   forall (s : t) (Hs : Sort s) (A : Set) (i : A) (f : elt -> A -> A),
+   forall (s : t) (Hs : Sort s) (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
   induction s.
@@ -1097,7 +1097,7 @@ Module Make (X: OrderedType) <: S with Module E := X.
  Definition min_elt (s : t) : option elt := Raw.min_elt s.
  Definition max_elt (s : t) : option elt := Raw.max_elt s.
  Definition choose (s : t) : option elt  := Raw.choose s.
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
+ Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
  Definition cardinal (s : t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s : t) : t :=
    Build_slist (Raw.filter_sort (sorted s) f).
@@ -1180,7 +1180,7 @@ Module Make (X: OrderedType) <: S with Module E := X.
   Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
   Proof. exact (fun H => Raw.diff_3 s.(sorted) s'.(sorted) H). Qed.
  
-  Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+  Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof. exact (Raw.fold_1 s.(sorted)). Qed.
 
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index e2a2cd45f6..7b25e8d61d 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -447,7 +447,7 @@ Module Properties (M: S).
   *)
 
   Lemma fold_0 : 
-      forall s (A : Set) (i : A) (f : elt -> A -> A),
+      forall s (A : Type) (i : A) (f : elt -> A -> A),
       exists l : list elt,
         NoDup l /\
         (forall x : elt, In x s <-> InA E.eq x l) /\
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v
index 81d148b4ed..960d82ce78 100644
--- a/theories/FSets/FSetWeakInterface.v
+++ b/theories/FSets/FSetWeakInterface.v
@@ -18,11 +18,11 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 
 (** Compatibility of a  boolean function with respect to an equality. *)
-Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) :=
+Definition compat_bool (A:Type)(eqA: A->A->Prop)(f: A-> bool) :=
   forall x y : A, eqA x y -> f x = f y.
 
 (** Compatibility of a predicate with respect to an equality. *)
-Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) :=
+Definition compat_P (A:Type)(eqA: A->A->Prop)(P : A -> Prop) :=
   forall x y : A, eqA x y -> P x -> P y.
 
 Hint Unfold compat_bool compat_P.
@@ -93,7 +93,7 @@ Module Type S.
   The order in which the elements of [s] are presented to [f]
   is unspecified. *)
 
-  Parameter fold : forall A : Set, (elt -> A -> A) -> t -> A -> A.
+  Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A.
   (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)],
   where [x1 ... xN] are the elements of [s].
   The order in which elements of [s] are presented to [f] is
@@ -187,7 +187,7 @@ Module Type S.
   Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s').
  
   (** Specification of [fold] *)  
-  Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+  Parameter fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
 
   (** Specification of [cardinal] *)  
diff --git a/theories/FSets/FSetWeakList.v b/theories/FSets/FSetWeakList.v
index 2b6017c5ed..0ca05c5d50 100644
--- a/theories/FSets/FSetWeakList.v
+++ b/theories/FSets/FSetWeakList.v
@@ -59,7 +59,7 @@ Module Raw (X: DecidableType).
         if X.eq_dec x y then l else y :: remove x l
     end.
 
-  Fixpoint fold (B : Set) (f : elt -> B -> B) (s : t) {struct s} : 
+  Fixpoint fold (B : Type) (f : elt -> B -> B) (s : t) {struct s} : 
    B -> B := fun i => match s with
                       | nil => i
                       | x :: l => fold f l (f x i)
@@ -293,7 +293,7 @@ Module Raw (X: DecidableType).
   Qed.
 
   Lemma fold_1 :
-   forall (s : t) (Hs : NoDup s) (A : Set) (i : A) (f : elt -> A -> A),
+   forall (s : t) (Hs : NoDup s) (A : Type) (i : A) (f : elt -> A -> A),
    fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof.
   induction s; simpl; auto; intros.
@@ -791,7 +791,7 @@ Module Make (X: DecidableType) <: S with Module E := X.
  Definition is_empty (s : t) : bool := Raw.is_empty s.
  Definition elements (s : t) : list elt := Raw.elements s.
  Definition choose (s:t) : option elt := Raw.choose s.
- Definition fold (B : Set) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
+ Definition fold (B : Type) (f : elt -> B -> B) (s : t) : B -> B := Raw.fold (B:=B) f s. 
  Definition cardinal (s : t) : nat := Raw.cardinal s.
  Definition filter (f : elt -> bool) (s : t) : t :=
    Build_slist (Raw.filter_unique (unique s) f).
@@ -872,7 +872,7 @@ Module Make (X: DecidableType) <: S with Module E := X.
   Lemma diff_3 : In x s -> ~ In x s' -> In x (diff s s').
   Proof. exact (fun H => Raw.diff_3 s.(unique) s'.(unique) H). Qed.
  
-  Lemma fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A),
+  Lemma fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A),
       fold f s i = fold_left (fun a e => f e a) (elements s) i.
   Proof. exact (Raw.fold_1 s.(unique)). Qed.