aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--theories/Logic/Eqdep.v4
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Logic/Eqdep.v b/theories/Logic/Eqdep.v
index 406429ffdf..ccd17ea946 100644
--- a/theories/Logic/Eqdep.v
+++ b/theories/Logic/Eqdep.v
@@ -33,5 +33,5 @@ Export EqdepTheory.
(** Exported hints *)
-Hint Resolve eq_dep_eq: core v62.
-Hint Resolve inj_pair2 inj_pairT2: core.
+Hint Resolve eq_dep_eq: eqdep v62.
+Hint Resolve inj_pair2 inj_pairT2: eqdep.