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, 3 insertions, 3 deletions

diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index f517898e1..55b00f063 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 *;