diff options
Diffstat (limited to 'theories/Structures/EqualitiesFacts.v')
| -rw-r--r-- | theories/Structures/EqualitiesFacts.v | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/theories/Structures/EqualitiesFacts.v b/theories/Structures/EqualitiesFacts.v index 7b6ee2eaca..c738b57f44 100644 --- a/theories/Structures/EqualitiesFacts.v +++ b/theories/Structures/EqualitiesFacts.v @@ -22,7 +22,7 @@ Module KeyDecidableType(D:DecidableType). Definition eqk {elt} : relation (key*elt) := D.eq @@1. Definition eqke {elt} : relation (key*elt) := D.eq * Logic.eq. - Hint Unfold eqk eqke. + Hint Unfold eqk eqke : core. (** eqk, eqke are equalities *) @@ -60,7 +60,7 @@ Module KeyDecidableType(D:DecidableType). Lemma eqk_1 {elt} k k' (e e':elt) : eqk (k,e) (k',e') -> D.eq k k'. Proof. trivial. Qed. - Hint Resolve eqke_1 eqke_2 eqk_1. + Hint Resolve eqke_1 eqke_2 eqk_1 : core. (* Additional facts *) @@ -69,7 +69,7 @@ Module KeyDecidableType(D:DecidableType). Proof. induction 1; firstorder. Qed. - Hint Resolve InA_eqke_eqk. + Hint Resolve InA_eqke_eqk : core. Lemma InA_eqk_eqke {elt} p (m:list (key*elt)) : InA eqk p m -> exists q, eqk p q /\ InA eqke q m. @@ -86,7 +86,7 @@ Module KeyDecidableType(D:DecidableType). Definition MapsTo {elt} (k:key)(e:elt):= InA eqke (k,e). Definition In {elt} k m := exists e:elt, MapsTo k e m. - Hint Unfold MapsTo In. + Hint Unfold MapsTo In : core. (* Alternative formulations for [In k l] *) @@ -167,9 +167,9 @@ Module KeyDecidableType(D:DecidableType). eauto with *. Qed. - Hint Extern 2 (eqke ?a ?b) => split. - Hint Resolve InA_eqke_eqk. - Hint Resolve In_inv_2 In_inv_3. + Hint Extern 2 (eqke ?a ?b) => split : core. + Hint Resolve InA_eqke_eqk : core. + Hint Resolve In_inv_2 In_inv_3 : core. End KeyDecidableType. |