diff options
| author | letouzey | 2007-05-27 19:57:03 +0000 |
|---|---|---|
| committer | letouzey | 2007-05-27 19:57:03 +0000 |
| commit | 25ebbaf1f325cf4e3694ab379f48a269d1d83d25 (patch) | |
| tree | 3dce1c387469f75ffd3fb7150bb871861adccd1c /theories/FSets/FMapWeakInterface.v | |
| parent | 5e7d37af933a6548b2194adb5ceeaff30e6bb3cb (diff) | |
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
Diffstat (limited to 'theories/FSets/FMapWeakInterface.v')
| -rw-r--r-- | theories/FSets/FMapWeakInterface.v | 4 |
1 files changed, 2 insertions, 2 deletions
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' := |