diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-27 19:57:03 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-05-27 19:57:03 +0000 |
| commit | 25ebbaf1f325cf4e3694ab379f48a269d1d83d25 (patch) | |
| tree | 3dce1c387469f75ffd3fb7150bb871861adccd1c /theories/FSets/FMapPositive.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/FMapPositive.v')
| -rw-r--r-- | theories/FSets/FMapPositive.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/FSets/FMapPositive.v b/theories/FSets/FMapPositive.v index af1e71de5..c3bdc773b 100644 --- a/theories/FSets/FMapPositive.v +++ b/theories/FSets/FMapPositive.v @@ -957,11 +957,11 @@ Module PositiveMap <: S with Module E:=PositiveOrderedTypeBits. Qed. - Definition fold (A B : Set) (f: positive -> A -> B -> B) (tr: t A) (v: B) := + Definition fold (A : Set)(B : Type) (f: positive -> A -> B -> B) (tr: t A) (v: B) := List.fold_left (fun a p => f (fst p) (snd p) a) (elements tr) v. Lemma fold_1 : - forall (A:Set)(m:t A)(B:Set)(i : B) (f : key -> A -> B -> B), + forall (A:Set)(m:t A)(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. intros; unfold fold; auto. |