diff options
Diffstat (limited to 'theories/FSets/FSetWeakInterface.v')
| -rw-r--r-- | theories/FSets/FSetWeakInterface.v | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/theories/FSets/FSetWeakInterface.v b/theories/FSets/FSetWeakInterface.v index 960d82ce78..72084d0340 100644 --- a/theories/FSets/FSetWeakInterface.v +++ b/theories/FSets/FSetWeakInterface.v @@ -17,16 +17,6 @@ Require Export DecidableType. Set Implicit Arguments. Unset Strict Implicit. -(** Compatibility of a boolean function with respect to an equality. *) -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: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. - (** * Non-dependent signature Signature [S] presents sets as purely informative programs |