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/FSetWeakInterface.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/FSetWeakInterface.v')
-rw-r--r-- | theories/FSets/FSetWeakInterface.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v index 81d148b4e..960d82ce7 100644 --- a/theories/FSets/FSetWeakInterface.v +++ b/theories/FSets/FSetWeakInterface.v @@ -18,11 +18,11 @@ Set Implicit Arguments. Unset Strict Implicit. (** Compatibility of a boolean function with respect to an equality. *) -Definition compat_bool (A:Set)(eqA: A->A->Prop)(f: A-> bool) := +Definition compat_bool (A:Type)(eqA: A->A->Prop)(f: A-> bool) := forall x y : A, eqA x y -> f x = f y. (** Compatibility of a predicate with respect to an equality. *) -Definition compat_P (A:Set)(eqA: A->A->Prop)(P : A -> Prop) := +Definition compat_P (A:Type)(eqA: A->A->Prop)(P : A -> Prop) := forall x y : A, eqA x y -> P x -> P y. Hint Unfold compat_bool compat_P. @@ -93,7 +93,7 @@ Module Type S. The order in which the elements of [s] are presented to [f] is unspecified. *) - Parameter fold : forall A : Set, (elt -> A -> A) -> t -> A -> A. + Parameter fold : forall A : Type, (elt -> A -> A) -> t -> A -> A. (** [fold f s a] computes [(f xN ... (f x2 (f x1 a))...)], where [x1 ... xN] are the elements of [s]. The order in which elements of [s] are presented to [f] is @@ -187,7 +187,7 @@ Module Type S. Parameter diff_3 : In x s -> ~ In x s' -> In x (diff s s'). (** Specification of [fold] *) - Parameter fold_1 : forall (A : Set) (i : A) (f : elt -> A -> A), + Parameter fold_1 : forall (A : Type) (i : A) (f : elt -> A -> A), fold f s i = fold_left (fun a e => f e a) (elements s) i. (** Specification of [cardinal] *) |