diff options
Diffstat (limited to 'theories/Structures/EqualitiesFacts.v')
| -rw-r--r-- | theories/Structures/EqualitiesFacts.v | 15 |
1 files changed, 1 insertions, 14 deletions
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index d9b1d76fd..d8a1b7581 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -8,21 +8,8 @@ Require Import Equalities Bool SetoidList RelationPairs. -(** In a BooleanEqualityType, [eqb] is compatible with [eq] *) - -Module BoolEqualityFacts (Import E : BooleanEqualityType). - -Instance eqb_compat : Proper (E.eq ==> E.eq ==> Logic.eq) eqb. -Proof. -intros x x' Exx' y y' Eyy'. -apply eq_true_iff_eq. -rewrite 2 eqb_eq, Exx', Eyy'; auto with *. -Qed. - -End BoolEqualityFacts. - - (** * Keys and datas used in FMap *) + Module KeyDecidableType(Import D:DecidableType). Section Elt. |