Rework of FSetProperties, in order to add more easily a Properties functor

for FMap (for the moment in FMapFacts).



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9890 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 0 insertions, 10 deletions

diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 6f23907b3..012f95d87 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -19,16 +19,6 @@ Set Implicit Arguments.
 Unset Strict Implicit.
 (* end hide *)
 
-(** 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