aboutsummaryrefslogtreecommitdiff
path: root/theories/Structures/Equalities.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Structures/Equalities.v')
-rw-r--r--theories/Structures/Equalities.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Structures/Equalities.v b/theories/Structures/Equalities.v
index 5f60a979c6..4143dba547 100644
--- a/theories/Structures/Equalities.v
+++ b/theories/Structures/Equalities.v
@@ -53,8 +53,8 @@ Module Type IsEqOrig (Import E:Eq').
Axiom eq_refl : forall x : t, x==x.
Axiom eq_sym : forall x y : t, x==y -> y==x.
Axiom eq_trans : forall x y z : t, x==y -> y==z -> x==z.
- Hint Immediate eq_sym.
- Hint Resolve eq_refl eq_trans.
+ Hint Immediate eq_sym : core.
+ Hint Resolve eq_refl eq_trans : core.
End IsEqOrig.
(** * Types with decidable equality *)