diff options
Diffstat (limited to 'theories/FSets/FMapFacts.v')
| -rw-r--r-- | theories/FSets/FMapFacts.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 7272421af7..9f9eca3c66 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -759,7 +759,8 @@ Module WProperties_fun (E:DecidableType)(M:WSfun E). Notation eqk := (@eq_key elt). Instance eqk_equiv : Equivalence eqk. - + Proof. unfold eq_key; split; eauto. Qed. + Instance eqke_equiv : Equivalence eqke. Proof. unfold eq_key_elt; split; repeat red; firstorder. |