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/FMapIntMap.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/FMapIntMap.v')
| -rw-r--r-- | theories/FSets/FMapIntMap.v | 4 |
1 files changed, 2 insertions, 2 deletions
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. |