diff options
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' := |