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

1 files changed, 7 insertions, 7 deletions

diff --git a/theories/FSets/FSetAVL.v b/theories/FSets/FSetAVL.v
index f21ae6e8c..f12a92e07 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.