aboutsummaryrefslogtreecommitdiff
path: root/theories/Classes/RelationPairs.v
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Classes/RelationPairs.v')
-rw-r--r--theories/Classes/RelationPairs.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Classes/RelationPairs.v b/theories/Classes/RelationPairs.v
index 7af2b0fc45..3e6358c8f3 100644
--- a/theories/Classes/RelationPairs.v
+++ b/theories/Classes/RelationPairs.v
@@ -157,6 +157,6 @@ Section RelProd_Instances.
Proof. unfold RelCompFun; firstorder. Qed.
End RelProd_Instances.
-Hint Unfold RelProd RelCompFun.
-Hint Extern 2 (RelProd _ _ _ _) => split.
+Hint Unfold RelProd RelCompFun : core.
+Hint Extern 2 (RelProd _ _ _ _) => split : core.