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/FSetProperties.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/FSetProperties.v')
| -rw-r--r-- | theories/FSets/FSetProperties.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v index e2a2cd45f..7b25e8d61 100644 --- a/theories/FSets/FSetProperties.v +++ b/theories/FSets/FSetProperties.v @@ -447,7 +447,7 @@ Module Properties (M: S). *) Lemma fold_0 : - forall s (A : Set) (i : A) (f : elt -> A -> A), + forall s (A : Type) (i : A) (f : elt -> A -> A), exists l : list elt, NoDup l /\ (forall x : elt, In x s <-> InA E.eq x l) /\ |