Merge PR #8987: Deprecate hint declaration/removal with no specified database

58 files changed, 305 insertions, 286 deletions

diff --git a/CHANGES.md b/CHANGES.md
index 9ee3c794d7..9a38b18a25 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -59,6 +59,10 @@ Tactics
   (e.g. `?[n]` or `?n` in terms - not in patterns) are now interpreted
   the same way as other variable names occurring in Ltac functions.
 
+- Hint declaration and removal should now specify a database (e.g. `Hint Resolve
+  foo : database`). When the database name is omitted, the hint is added to the
+  core database (as previously), but a deprecation warning is emitted.
+
 Vernacular commands
 
 - `Combined Scheme` can now work when inductive schemes are generated in sort
diff --git a/plugins/btauto/Algebra.v b/plugins/btauto/Algebra.v
index f1095fc9f1..638a4cef21 100644
--- a/plugins/btauto/Algebra.v
+++ b/plugins/btauto/Algebra.v
@@ -10,7 +10,7 @@ end.
 
 Arguments decide P /H.
 
-Hint Extern 5 => progress bool.
+Hint Extern 5 => progress bool : core.
 
 Ltac define t x H :=
 set (x := t) in *; assert (H : t = x) by reflexivity; clearbody x.
@@ -147,7 +147,7 @@ Qed.
 
 (** * The core reflexive part. *)
 
-Hint Constructors valid.
+Hint Constructors valid : core.
 
 Fixpoint beq_poly pl pr :=
 match pl with
@@ -315,7 +315,7 @@ Section Validity.
 
 (* Decision procedure of validity *)
 
-Hint Constructors valid linear.
+Hint Constructors valid linear : core.
 
 Lemma valid_le_compat : forall k l p, valid k p -> (k <= l)%positive -> valid l p.
 Proof.
@@ -425,10 +425,10 @@ match goal with
 | [ |- (?z < Pos.max ?x ?y)%positive ] =>
   apply Pos.max_case_strong; intros; lia
 | _ => zify; omega
-end.
-Hint Resolve Pos.le_max_r Pos.le_max_l.
+end : core.
+Hint Resolve Pos.le_max_r Pos.le_max_l : core.
 
-Hint Constructors valid linear.
+Hint Constructors valid linear : core.
 
 (* Compatibility of validity w.r.t algebraic operations *)
 
diff --git a/plugins/btauto/Reflect.v b/plugins/btauto/Reflect.v
index 4cde08872f..98f5ab067a 100644
--- a/plugins/btauto/Reflect.v
+++ b/plugins/btauto/Reflect.v
@@ -77,10 +77,10 @@ intros var f; induction f; simpl poly_of_formula; simpl formula_eval; auto.
   end.
 Qed.
 
-Hint Extern 5 => change 0 with (min 0 0).
-Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat.
-Local Hint Constructors valid.
-Hint Extern 5 => zify; omega.
+Hint Extern 5 => change 0 with (min 0 0) : core.
+Local Hint Resolve poly_add_valid_compat poly_mul_valid_compat : core.
+Local Hint Constructors valid : core.
+Hint Extern 5 => zify; omega : core.
 
 (* Compatibility with validity *)
 
diff --git a/plugins/ssr/ssrbool.v b/plugins/ssr/ssrbool.v
index a618fc781f..3a7cf41d43 100644
--- a/plugins/ssr/ssrbool.v
+++ b/plugins/ssr/ssrbool.v
@@ -371,7 +371,7 @@ Ltac prop_congr := apply: prop_congr.
 Lemma is_true_true : true.               Proof. by []. Qed.
 Lemma not_false_is_true : ~ false.       Proof. by []. Qed.
 Lemma is_true_locked_true : locked true. Proof. by unlock. Qed.
-Hint Resolve is_true_true not_false_is_true is_true_locked_true.
+Hint Resolve is_true_true not_false_is_true is_true_locked_true : core.
 
 (**  Shorter names.  **)
 Definition isT := is_true_true.
diff --git a/plugins/ssr/ssrfun.v b/plugins/ssr/ssrfun.v
index e2c0ed7c8b..6535cad8b7 100644
--- a/plugins/ssr/ssrfun.v
+++ b/plugins/ssr/ssrfun.v
@@ -398,7 +398,7 @@ End ExtensionalEquality.
 Typeclasses Opaque eqfun.
 Typeclasses Opaque eqrel.
 
-Hint Resolve frefl rrefl.
+Hint Resolve frefl rrefl : core.
 
 Notation "f1 =1 f2" := (eqfun f1 f2)
   (at level 70, no associativity) : fun_scope.
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 2f2d32e887..328d57c8a3 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1373,10 +1373,10 @@ let interp_hints poly =
       let _, tacexp = Genintern.generic_intern env tacexp in
       HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp)
 
-let add_hints ~local dbnames0 h =
-  if String.List.mem "nocore" dbnames0 then
+let add_hints ~local dbnames h =
+  if String.List.mem "nocore" dbnames then
     user_err Pp.(str "The hint database \"nocore\" is meant to stay empty.");
-  let dbnames = if List.is_empty dbnames0 then ["core"] else dbnames0 in
+  assert (not (List.is_empty dbnames));
   let env = Global.env() in
   let sigma = Evd.from_env env in
   match h with
diff --git a/theories/Bool/Bool.v b/theories/Bool/Bool.v
index 42af3583d4..075288e216 100644
--- a/theories/Bool/Bool.v
+++ b/theories/Bool/Bool.v
@@ -48,7 +48,7 @@ Proof.
   discriminate.
 Qed.
 Hint Resolve diff_false_true : bool.
-Hint Extern 1 (false <> true) => exact diff_false_true.
+Hint Extern 1 (false <> true) => exact diff_false_true : core.
 
 Lemma eq_true_false_abs : forall b:bool, b = true -> b = false -> False.
 Proof.
@@ -621,7 +621,7 @@ Lemma absurd_eq_true : forall b, False -> b = true.
 Proof.
   contradiction.
 Qed.
-Hint Resolve absurd_eq_true.
+Hint Resolve absurd_eq_true : core.
 
 (* A specific instance of eq_trans that preserves compatibility with
    old hint bool_2 *)
@@ -630,7 +630,7 @@ Lemma trans_eq_bool : forall x y z:bool, x = y -> y = z -> x = z.
 Proof.
   apply eq_trans.
 Qed.
-Hint Resolve trans_eq_bool.
+Hint Resolve trans_eq_bool : core.
 
 (*****************************************)
 (** * Reflection of [bool] into [Prop] *)
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.
 
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index b0d1824827..8fc04d81e6 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -41,7 +41,7 @@ Local Open Scope Int_scope.
 Local Notation int := I.t.
 
 Definition key := X.t.
-Hint Transparent key.
+Hint Transparent key : core.
 
 (** * Trees *)
 
@@ -488,8 +488,8 @@ Functional Scheme map2_opt_ind := Induction for map2_opt Sort Prop.
 
 (** * Automation and dedicated tactics. *)
 
-Hint Constructors tree MapsTo In bst.
-Hint Unfold lt_tree gt_tree.
+Hint Constructors tree MapsTo In bst : core.
+Hint Unfold lt_tree gt_tree : core.
 
 Tactic Notation "factornode" ident(l) ident(x) ident(d) ident(r) ident(h)
  "as" ident(s) :=
@@ -569,7 +569,7 @@ Lemma MapsTo_In : forall k e m, MapsTo k e m -> In k m.
 Proof.
  induction 1; auto.
 Qed.
-Hint Resolve MapsTo_In.
+Hint Resolve MapsTo_In : core.
 
 Lemma In_MapsTo : forall k m, In k m -> exists e, MapsTo k e m.
 Proof.
@@ -588,7 +588,7 @@ Lemma MapsTo_1 :
 Proof.
  induction m; simpl; intuition_in; eauto.
 Qed.
-Hint Immediate MapsTo_1.
+Hint Immediate MapsTo_1 : core.
 
 Lemma In_1 :
  forall m x y, X.eq x y -> In x m -> In y m.
@@ -627,7 +627,7 @@ Proof.
  unfold gt_tree in *; intuition_in; order.
 Qed.
 
-Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
 
 Lemma lt_left : forall x y l r e h,
  lt_tree x (Node l y e r h) -> lt_tree x l.
@@ -653,7 +653,7 @@ Proof.
  intuition_in.
 Qed.
 
-Hint Resolve lt_left lt_right gt_left gt_right.
+Hint Resolve lt_left lt_right gt_left gt_right : core.
 
 Lemma lt_tree_not_in :
  forall x m, lt_tree x m -> ~ In x m.
@@ -679,7 +679,7 @@ Proof.
  eauto.
 Qed.
 
-Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
 
 (** * Empty map *)
 
@@ -811,7 +811,7 @@ Lemma create_bst :
 Proof.
  unfold create; auto.
 Qed.
-Hint Resolve create_bst.
+Hint Resolve create_bst : core.
 
 Lemma create_in :
  forall l x e r y,
@@ -828,7 +828,7 @@ Proof.
  (apply lt_tree_node || apply gt_tree_node); auto;
  (eapply lt_tree_trans || eapply gt_tree_trans); eauto. 
 Qed.
-Hint Resolve bal_bst.
+Hint Resolve bal_bst : core.
 
 Lemma bal_in : forall l x e r y,
  In y (bal l x e r) <-> X.eq y x \/ In y l \/ In y r.
@@ -869,7 +869,7 @@ Proof.
  apply MX.eq_lt with x; auto.
  apply MX.lt_eq with x; auto.
 Qed.
-Hint Resolve add_bst.
+Hint Resolve add_bst : core.
 
 Lemma add_1 : forall m x y e, X.eq x y -> MapsTo y e (add x e m).
 Proof.
@@ -949,7 +949,7 @@ Proof.
  destruct 1.
  apply H2; intuition.
 Qed.
-Hint Resolve remove_min_bst.
+Hint Resolve remove_min_bst : core.
 
 Lemma remove_min_gt_tree : forall l x e r h,
  bst (Node l x e r h) ->
@@ -968,7 +968,7 @@ Proof.
  assert (X.lt m#1 x) by order.
  decompose [or] H; order.
 Qed.
-Hint Resolve remove_min_gt_tree.
+Hint Resolve remove_min_gt_tree : core.
 
 Lemma remove_min_find : forall l x e r h y,
  bst (Node l x e r h) ->
@@ -1120,7 +1120,7 @@ Proof.
  intuition; [ apply MX.lt_eq with x | ]; eauto.
  intuition; [ apply MX.eq_lt with x | ]; eauto.
 Qed.
-Hint Resolve join_bst.
+Hint Resolve join_bst : core.
 
 Lemma join_find : forall l x d r y,
  bst l -> bst r -> lt_tree x l -> gt_tree x r ->
@@ -1256,7 +1256,7 @@ Proof.
  rewrite remove_min_in, e1; simpl; auto.
  change (gt_tree (m2',xd)#2#1 (m2',xd)#1). rewrite <-e1; eauto.
 Qed.
-Hint Resolve concat_bst.
+Hint Resolve concat_bst : core.
 
 Lemma concat_find : forall m1 m2 y, bst m1 -> bst m2 ->
  (forall y1 y2, In y1 m1 -> In y2 m2 -> X.lt y1 y2) ->
@@ -1344,7 +1344,7 @@ Proof.
  intros; unfold elements; apply elements_aux_sort; auto.
  intros; inversion H0.
 Qed.
-Hint Resolve elements_sort.
+Hint Resolve elements_sort : core.
 
 Lemma elements_nodup : forall s : t elt, bst s -> NoDupA eqk (elements s).
 Proof.
@@ -1612,7 +1612,7 @@ destruct (map_option_2 H) as (d0 & ? & ?).
 destruct (map_option_2 H') as (d0' & ? & ?).
 eapply X.lt_trans with x; eauto using MapsTo_In.
 Qed.
-Hint Resolve map_option_bst.
+Hint Resolve map_option_bst : core.
 
 Ltac nonify e :=
  replace e with (@None elt) by
@@ -1711,7 +1711,7 @@ apply X.lt_trans with x1.
 destruct (map2_opt_2 H1 H6 Hy); intuition.
 destruct (map2_opt_2 H2 H7 Hy'); intuition.
 Qed.
-Hint Resolve map2_opt_bst.
+Hint Resolve map2_opt_bst : core.
 
 Ltac map2_aux :=
  match goal with
@@ -2066,7 +2066,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; P.MX.elim_comp; auto.
   Qed.
-  Hint Resolve cons_Cmp.
+  Hint Resolve cons_Cmp : core.
 
   Lemma compare_end_Cmp :
    forall e2, Cmp (compare_end e2) nil (P.flatten_e e2).
diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v
index 2d5a79838a..d19c5558d8 100644
--- a/theories/FSets/FMapFacts.v
+++ b/theories/FSets/FMapFacts.v
@@ -20,7 +20,7 @@ Require Export FMapInterface.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Extern 1 (Equivalence _) => constructor; congruence.
+Hint Extern 1 (Equivalence _) => constructor; congruence : core.
 
 (** * Facts about weak maps *)
 
diff --git a/theories/FSets/FMapFullAVL.v b/theories/FSets/FMapFullAVL.v
index c0db8646c7..950b30ee4d 100644
--- a/theories/FSets/FMapFullAVL.v
+++ b/theories/FSets/FMapFullAVL.v
@@ -63,7 +63,7 @@ Inductive avl : t elt -> Prop :=
 
 (** * Automation and dedicated tactics about [avl]. *)
 
-Hint Constructors avl.
+Hint Constructors avl : core.
 
 Lemma height_non_negative : forall (s : t elt), avl s ->
  height s >= 0.
@@ -100,7 +100,7 @@ Lemma avl_node : forall x e l r, avl l -> avl r ->
 Proof.
   intros; auto.
 Qed.
-Hint Resolve avl_node.
+Hint Resolve avl_node : core.
 
 (** Results about [height] *)
 
@@ -193,7 +193,7 @@ Lemma add_avl : forall m x e, avl m -> avl (add x e m).
 Proof.
  intros; generalize (add_avl_1 x e H); intuition.
 Qed.
-Hint Resolve add_avl.
+Hint Resolve add_avl : core.
 
 (** * Extraction of minimum binding *)
 
@@ -274,7 +274,7 @@ Lemma remove_avl : forall m x, avl m -> avl (remove x m).
 Proof.
  intros; generalize (remove_avl_1 x H); intuition.
 Qed.
-Hint Resolve remove_avl.
+Hint Resolve remove_avl : core.
 
 
 (** * Join *)
@@ -331,7 +331,7 @@ Lemma join_avl : forall l x d r, avl l -> avl r -> avl (join l x d r).
 Proof.
  intros; destruct (join_avl_1 x d H H0); auto.
 Qed.
-Hint Resolve join_avl.
+Hint Resolve join_avl : core.
 
 (** concat *)
 
@@ -341,7 +341,7 @@ Proof.
  intros; apply join_avl; auto.
  generalize (remove_min_avl H0); rewrite e1; simpl; auto.
 Qed.
-Hint Resolve concat_avl.
+Hint Resolve concat_avl : core.
 
 (** split *)
 
@@ -355,7 +355,7 @@ Proof.
 Qed.
 
 End Elt.
-Hint Constructors avl.
+Hint Constructors avl : core.
 
 Section Map.
 Variable elt elt' : Type.
@@ -713,7 +713,7 @@ Module IntMake_ord (I:Int)(X: OrderedType)(D : OrderedType) <:
   Proof.
    destruct c; simpl; intros; MX.elim_comp; auto.
   Qed.
-  Hint Resolve cons_Cmp.
+  Hint Resolve cons_Cmp : core.
 
   Lemma compare_aux_Cmp : forall e,
    Cmp (compare_aux e) (flatten_e (fst e)) (flatten_e (snd e)).
diff --git a/theories/FSets/FMapInterface.v b/theories/FSets/FMapInterface.v
index 38a96dc393..8970529103 100644
--- a/theories/FSets/FMapInterface.v
+++ b/theories/FSets/FMapInterface.v
@@ -58,7 +58,7 @@ Definition Cmp (elt:Type)(cmp:elt->elt->bool) e1 e2 := cmp e1 e2 = true.
 Module Type WSfun (E : DecidableType).
 
   Definition key := E.t.
-  Hint Transparent key.
+  Hint Transparent key : core.
 
   Parameter t : Type -> Type.
   (** the abstract type of maps *)
diff --git a/theories/FSets/FMapList.v b/theories/FSets/FMapList.v
index 3e98d11976..6ca158a277 100644
--- a/theories/FSets/FMapList.v
+++ b/theories/FSets/FMapList.v
@@ -51,7 +51,7 @@ Proof.
  intro abs.
  inversion abs.
 Qed.
-Hint Resolve empty_1.
+Hint Resolve empty_1 : core.
 
 Lemma empty_sorted : Sort empty.
 Proof.
@@ -216,7 +216,7 @@ Proof.
  compute in H0,H1.
  simpl; case (X.compare x x''); intuition.
 Qed.
-Hint Resolve add_Inf.
+Hint Resolve add_Inf : core.
 
 Lemma add_sorted : forall m (Hm:Sort m) x e, Sort (add x e m).
 Proof.
@@ -302,7 +302,7 @@ Proof.
  inversion_clear Hm.
  apply Inf_lt with (x'',e''); auto.
 Qed.
-Hint Resolve remove_Inf.
+Hint Resolve remove_Inf : core.
 
 Lemma remove_sorted : forall m (Hm:Sort m) x, Sort (remove x m).
 Proof.
@@ -586,7 +586,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
-Hint Resolve map_lelistA.
+Hint Resolve map_lelistA : core.
 
 Lemma map_sorted : forall (m: t elt)(Hm : sort (@ltk elt) m)(f:elt -> elt'),
   sort (@ltk elt') (map f m).
@@ -654,7 +654,7 @@ Proof.
  inversion_clear H; auto.
 Qed.
 
-Hint Resolve mapi_lelistA.
+Hint Resolve mapi_lelistA : core.
 
 Lemma mapi_sorted : forall m (Hm : sort (@ltk elt) m)(f: key ->elt -> elt'),
   sort (@ltk elt') (mapi f m).
@@ -781,7 +781,7 @@ Proof.
  inversion_clear H; auto.
  inversion_clear H0; auto.
 Qed.
-Hint Resolve combine_lelistA.
+Hint Resolve combine_lelistA : core.
 
 Lemma combine_sorted :
   forall m (Hm : sort (@ltk elt) m) m' (Hm' : sort (@ltk elt') m'),
diff --git a/theories/FSets/FMapWeakList.v b/theories/FSets/FMapWeakList.v
index 6736096509..03dce9666d 100644
--- a/theories/FSets/FMapWeakList.v
+++ b/theories/FSets/FMapWeakList.v
@@ -49,7 +49,7 @@ Proof.
  inversion abs.
 Qed.
 
-Hint Resolve empty_1.
+Hint Resolve empty_1 : core.
 
 Lemma empty_NoDup : NoDupA empty.
 Proof.
@@ -621,7 +621,7 @@ Proof.
  inversion_clear 1.
  intros; apply add_NoDup; auto.
 Qed.
-Hint Resolve fold_right_pair_NoDup.
+Hint Resolve fold_right_pair_NoDup : core.
 
 Lemma combine_NoDup :
   forall m (Hm:NoDupA (@eqk elt) m) m' (Hm':NoDupA (@eqk elt') m'),
diff --git a/theories/FSets/FSetBridge.v b/theories/FSets/FSetBridge.v
index 0c4ecb1f31..3952c28061 100644
--- a/theories/FSets/FSetBridge.v
+++ b/theories/FSets/FSetBridge.v
@@ -137,7 +137,7 @@ Module DepOfNodep (Import M: S) <: Sdep with Module E := M.E.
     generalize (E.eq_sym H0); case (Pdec x); case (Pdec y); firstorder.
   Qed.
 
-  Hint Resolve compat_P_aux.
+  Hint Resolve compat_P_aux : core.
 
   Definition filter :
     forall (P : elt -> Prop) (Pdec : forall x : elt, {P x} + {~ P x}) (s : t),
@@ -467,7 +467,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
   Proof.
     intros; unfold elements; case (M.elements s); firstorder.
   Qed.
-  Hint Resolve elements_3.
+  Hint Resolve elements_3 : core.
 
   Lemma elements_3w : forall s : t, NoDupA E.eq (elements s).
   Proof. auto. Qed.
@@ -666,7 +666,7 @@ Module NodepOfDep (M: Sdep) <: S with Module E := M.E.
       rewrite <- H1; firstorder.
   Qed.
 
-  Hint Resolve compat_P_aux.
+  Hint Resolve compat_P_aux : core.
 
   Definition filter (f : elt -> bool) (s : t) : t :=
     let (s', _) := filter (P:=fun x => f x = true) (f_dec f) s in s'.
diff --git a/theories/FSets/FSetInterface.v b/theories/FSets/FSetInterface.v
index 0926d3ae9f..fa7f1c5f4e 100644
--- a/theories/FSets/FSetInterface.v
+++ b/theories/FSets/FSetInterface.v
@@ -253,7 +253,7 @@ Module Type WSfun (E : DecidableType).
 
   End Spec.
 
-  Hint Transparent elt.
+  Hint Transparent elt : core.
   Hint Resolve mem_1 equal_1 subset_1 empty_1
     is_empty_1 choose_1 choose_2 add_1 add_2 remove_1
     remove_2 singleton_2 union_1 union_2 union_3
diff --git a/theories/FSets/FSetProperties.v b/theories/FSets/FSetProperties.v
index c9cfb94ace..17f0e25e7a 100644
--- a/theories/FSets/FSetProperties.v
+++ b/theories/FSets/FSetProperties.v
@@ -21,8 +21,8 @@ Require Import DecidableTypeEx FSetFacts FSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Unfold transpose compat_op Proper respectful.
-Hint Extern 1 (Equivalence _) => constructor; congruence.
+Hint Unfold transpose compat_op Proper respectful : core.
+Hint Extern 1 (Equivalence _) => constructor; congruence : core.
 
 (** First, a functor for Weak Sets in functorial version. *)
 
@@ -732,7 +732,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
-  Hint Resolve cardinal_inv_1.
+  Hint Resolve cardinal_inv_1 : core.
 
   Lemma cardinal_inv_2 :
    forall s n, cardinal s = S n -> { x : elt | In x s }.
@@ -769,7 +769,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   exact Equal_cardinal.
   Qed.
 
-  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.
 
   (** ** Cardinal and set operators *)
 
@@ -887,7 +887,7 @@ Module WProperties_fun (Import E : DecidableType)(M : WSfun E).
   auto with set.
   Qed.
 
-  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
+  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.
 
 End WProperties_fun.
 
@@ -952,7 +952,7 @@ Module OrdProperties (M:S).
    red; intros x a b H; unfold leb.
    f_equal; apply gtb_compat; auto.
   Qed.
-  Hint Resolve gtb_compat leb_compat.
+  Hint Resolve gtb_compat leb_compat : core.
 
   Lemma elements_split : forall x s,
    elements s = elements_lt x s ++ elements_ge x s.
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 75f14bb4da..7f0387dd12 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -136,7 +136,7 @@ Defined.
 Inductive BoolSpec (P Q : Prop) : bool -> Prop :=
   | BoolSpecT : P -> BoolSpec P Q true
   | BoolSpecF : Q -> BoolSpec P Q false.
-Hint Constructors BoolSpec.
+Hint Constructors BoolSpec : core.
 
 
 (********************************************************************)
@@ -344,7 +344,7 @@ Inductive CompareSpec (Peq Plt Pgt : Prop) : comparison -> Prop :=
  | CompEq : Peq -> CompareSpec Peq Plt Pgt Eq
  | CompLt : Plt -> CompareSpec Peq Plt Pgt Lt
  | CompGt : Pgt -> CompareSpec Peq Plt Pgt Gt.
-Hint Constructors CompareSpec.
+Hint Constructors CompareSpec : core.
 
 (** For having clean interfaces after extraction, [CompareSpec] is declared
     in Prop. For some situations, it is nonetheless useful to have a
@@ -354,7 +354,7 @@ Inductive CompareSpecT (Peq Plt Pgt : Prop) : comparison -> Type :=
  | CompEqT : Peq -> CompareSpecT Peq Plt Pgt Eq
  | CompLtT : Plt -> CompareSpecT Peq Plt Pgt Lt
  | CompGtT : Pgt -> CompareSpecT Peq Plt Pgt Gt.
-Hint Constructors CompareSpecT.
+Hint Constructors CompareSpecT : core.
 
 Lemma CompareSpec2Type : forall Peq Plt Pgt c,
  CompareSpec Peq Plt Pgt c -> CompareSpecT Peq Plt Pgt c.
@@ -371,7 +371,7 @@ Definition CompSpec {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Prop :=
 
 Definition CompSpecT {A} (eq lt : A->A->Prop)(x y:A) : comparison -> Type :=
  CompareSpecT (eq x y) (lt x y) (lt y x).
-Hint Unfold CompSpec CompSpecT.
+Hint Unfold CompSpec CompSpecT : core.
 
 Lemma CompSpec2Type : forall A (eq lt:A->A->Prop) x y c,
  CompSpec eq lt x y c -> CompSpecT eq lt x y c.
diff --git a/theories/Lists/List.v b/theories/Lists/List.v
index 4614d215eb..d5241e622c 100644
--- a/theories/Lists/List.v
+++ b/theories/Lists/List.v
@@ -219,7 +219,7 @@ Section Facts.
   Proof.
      auto using app_assoc.
   Qed.
-  Hint Resolve app_assoc_reverse.
+  Hint Resolve app_assoc_reverse : core.
   (* end hide *)
 
   (** [app] commutes with [cons] *)
@@ -1569,19 +1569,19 @@ Section SetIncl.
   Variable A : Type.
 
   Definition incl (l m:list A) := forall a:A, In a l -> In a m.
-  Hint Unfold incl.
+  Hint Unfold incl : core.
 
   Lemma incl_refl : forall l:list A, incl l l.
   Proof.
     auto.
   Qed.
-  Hint Resolve incl_refl.
+  Hint Resolve incl_refl : core.
 
   Lemma incl_tl : forall (a:A) (l m:list A), incl l m -> incl l (a :: m).
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_tl.
+  Hint Immediate incl_tl : core.
 
   Lemma incl_tran : forall l m n:list A, incl l m -> incl m n -> incl l n.
   Proof.
@@ -1592,13 +1592,13 @@ Section SetIncl.
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_appl.
+  Hint Immediate incl_appl : core.
 
   Lemma incl_appr : forall l m n:list A, incl l n -> incl l (m ++ n).
   Proof.
     auto with datatypes.
   Qed.
-  Hint Immediate incl_appr.
+  Hint Immediate incl_appr : core.
 
   Lemma incl_cons :
     forall (a:A) (l m:list A), In a m -> incl l m -> incl (a :: l) m.
@@ -1613,7 +1613,7 @@ Section SetIncl.
     now_show (In a0 l -> In a0 m).
     auto.
   Qed.
-  Hint Resolve incl_cons.
+  Hint Resolve incl_cons : core.
 
   Lemma incl_app : forall l m n:list A, incl l n -> incl m n -> incl (l ++ m) n.
   Proof.
@@ -1621,7 +1621,7 @@ Section SetIncl.
     now_show (In a n).
     elim (in_app_or _ _ _ H1); auto.
   Qed.
-  Hint Resolve incl_app.
+  Hint Resolve incl_app : core.
 
 End SetIncl.
 
@@ -2180,7 +2180,7 @@ Section Exists_Forall.
       | Exists_cons_hd : forall x l, P x -> Exists (x::l)
       | Exists_cons_tl : forall x l, Exists l -> Exists (x::l).
 
-    Hint Constructors Exists.
+    Hint Constructors Exists : core.
 
     Lemma Exists_exists (l:list A) :
       Exists l <-> (exists x, In x l /\ P x).
@@ -2214,7 +2214,7 @@ Section Exists_Forall.
       | Forall_nil : Forall nil
       | Forall_cons : forall x l, P x -> Forall l -> Forall (x::l).
 
-    Hint Constructors Forall.
+    Hint Constructors Forall : core.
 
     Lemma Forall_forall (l:list A):
       Forall l <-> (forall x, In x l -> P x).
@@ -2299,8 +2299,8 @@ Section Exists_Forall.
 
 End Exists_Forall.
 
-Hint Constructors Exists.
-Hint Constructors Forall.
+Hint Constructors Exists : core.
+Hint Constructors Forall : core.
 
 Section Forall2.
 
@@ -2314,7 +2314,7 @@ Section Forall2.
     | Forall2_cons : forall x y l l',
       R x y -> Forall2 l l' -> Forall2 (x::l) (y::l').
 
-  Hint Constructors Forall2.
+  Hint Constructors Forall2 : core.
 
   Theorem Forall2_refl : Forall2 [] [].
   Proof. intros; apply Forall2_nil. Qed.
@@ -2348,7 +2348,7 @@ Section Forall2.
   Qed.
 End Forall2.
 
-Hint Constructors Forall2.
+Hint Constructors Forall2 : core.
 
 Section ForallPairs.
 
@@ -2369,7 +2369,7 @@ Section ForallPairs.
     | FOP_cons : forall a l,
       Forall (R a) l -> ForallOrdPairs l -> ForallOrdPairs (a::l).
 
-  Hint Constructors ForallOrdPairs.
+  Hint Constructors ForallOrdPairs : core.
 
   Lemma ForallOrdPairs_In : forall l,
     ForallOrdPairs l ->
diff --git a/theories/Lists/ListSet.v b/theories/Lists/ListSet.v
index cc7d6f5536..3afdd8df27 100644
--- a/theories/Lists/ListSet.v
+++ b/theories/Lists/ListSet.v
@@ -193,7 +193,7 @@ Section first_definitions.
      | auto with datatypes ].
   Qed.
 
-  Hint Resolve set_add_intro1 set_add_intro2.
+  Hint Resolve set_add_intro1 set_add_intro2 : core.
 
   Lemma set_add_intro :
    forall (a b:A) (x:set), a = b \/ set_In a x -> set_In a (set_add b x).
@@ -224,7 +224,7 @@ Section first_definitions.
    case H1; trivial.
    Qed.
 
-  Hint Resolve set_add_intro set_add_elim set_add_elim2.
+  Hint Resolve set_add_intro set_add_elim set_add_elim2 : core.
 
   Lemma set_add_not_empty : forall (a:A) (x:set), set_add a x <> empty_set.
   Proof.
@@ -310,7 +310,7 @@ Section first_definitions.
     intros; elim H0; auto with datatypes.
   Qed.
 
-  Hint Resolve set_union_intro2 set_union_intro1.
+  Hint Resolve set_union_intro2 set_union_intro1 : core.
 
   Lemma set_union_intro :
    forall (a:A) (x y:set),
@@ -393,7 +393,7 @@ Section first_definitions.
     eauto with datatypes.
   Qed.
 
-  Hint Resolve set_inter_elim1 set_inter_elim2.
+  Hint Resolve set_inter_elim1 set_inter_elim2 : core.
 
   Lemma set_inter_elim :
    forall (a:A) (x y:set),
@@ -471,7 +471,7 @@ Section first_definitions.
   apply (set_diff_elim1 _ _ _ H).
   Qed.
 
-Hint Resolve set_diff_intro set_diff_trivial.
+Hint Resolve set_diff_intro set_diff_trivial : core.
 
 
 End first_definitions.
diff --git a/theories/Lists/SetoidList.v b/theories/Lists/SetoidList.v
index 0c5fe55b27..cab4c23df1 100644
--- a/theories/Lists/SetoidList.v
+++ b/theories/Lists/SetoidList.v
@@ -30,7 +30,7 @@ Inductive InA (x : A) : list A -> Prop :=
   | InA_cons_hd : forall y l, eqA x y -> InA x (y :: l)
   | InA_cons_tl : forall y l, InA x l -> InA x (y :: l).
 
-Hint Constructors InA.
+Hint Constructors InA : core.
 
 (** TODO: it would be nice to have a generic definition instead
     of the previous one. Having [InA = Exists eqA] raises too
@@ -62,7 +62,7 @@ Inductive NoDupA : list A -> Prop :=
   | NoDupA_nil : NoDupA nil
   | NoDupA_cons : forall x l, ~ InA x l -> NoDupA l -> NoDupA (x::l).
 
-Hint Constructors NoDupA.
+Hint Constructors NoDupA : core.
 
 (** An alternative definition of [NoDupA] based on [ForallOrdPairs] *)
 
@@ -93,7 +93,7 @@ Inductive eqlistA : list A -> list A -> Prop :=
   | eqlistA_cons : forall x x' l l',
       eqA x x' -> eqlistA l l' -> eqlistA (x::l) (x'::l').
 
-Hint Constructors eqlistA.
+Hint Constructors eqlistA : core.
 
 (** We could also have written [eqlistA = Forall2 eqA]. *)
 
@@ -107,8 +107,8 @@ Definition eqarefl := (@Equivalence_Reflexive _ _ eqA_equiv).
 Definition eqatrans := (@Equivalence_Transitive _ _ eqA_equiv).
 Definition eqasym := (@Equivalence_Symmetric _ _ eqA_equiv).
  
-Hint Resolve eqarefl eqatrans.
-Hint Immediate eqasym.
+Hint Resolve eqarefl eqatrans : core.
+Hint Immediate eqasym : core.
 
 Ltac inv := invlist InA; invlist sort; invlist lelistA; invlist NoDupA.
 
@@ -154,14 +154,14 @@ Lemma InA_eqA : forall l x y, eqA x y -> InA x l -> InA y l.
 Proof.
  intros l x y H H'. rewrite <- H. auto.
 Qed.
-Hint Immediate InA_eqA.
+Hint Immediate InA_eqA : core.
 
 Lemma In_InA : forall l x, In x l -> InA x l.
 Proof.
  simple induction l; simpl; intuition.
  subst; auto.
 Qed.
-Hint Resolve In_InA.
+Hint Resolve In_InA : core.
 
 Lemma InA_split : forall l x, InA x l ->
  exists l1 y l2, eqA x y /\ l = l1++y::l2.
@@ -786,12 +786,12 @@ Hypothesis ltA_compat : Proper (eqA==>eqA==>iff) ltA.
 
 Let sotrans := (@StrictOrder_Transitive _ _ ltA_strorder).
 
-Hint Resolve sotrans.
+Hint Resolve sotrans : core.
 
 Notation InfA:=(lelistA ltA).
 Notation SortA:=(sort ltA).
 
-Hint Constructors lelistA sort.
+Hint Constructors lelistA sort : core.
 
 Lemma InfA_ltA :
  forall l x y, ltA x y -> InfA y l -> InfA x l.
@@ -814,7 +814,7 @@ Lemma InfA_eqA l x y : eqA x y -> InfA y l -> InfA x l.
 Proof using eqA_equiv ltA_compat.
  intros H; now rewrite H.
 Qed.
-Hint Immediate InfA_ltA InfA_eqA.
+Hint Immediate InfA_ltA InfA_eqA : core.
 
 Lemma SortA_InfA_InA :
  forall l x a, SortA l -> InfA a l -> InA x l -> ltA a x.
@@ -1005,7 +1005,7 @@ Qed.
 End Filter.
 End Type_with_equality.
 
-Hint Constructors InA eqlistA NoDupA sort lelistA.
+Hint Constructors InA eqlistA NoDupA sort lelistA : core.
 
 Arguments equivlistA_cons_nil {A} eqA {eqA_equiv} x l _.
 Arguments equivlistA_nil_eq {A} eqA {eqA_equiv} l _.
diff --git a/theories/Lists/SetoidPermutation.v b/theories/Lists/SetoidPermutation.v
index 24b96514fd..f5ea303343 100644
--- a/theories/Lists/SetoidPermutation.v
+++ b/theories/Lists/SetoidPermutation.v
@@ -28,7 +28,7 @@ Inductive PermutationA : list A -> list A -> Prop :=
   | permA_swap x y l : PermutationA (y :: x :: l) (x :: y :: l)
   | permA_trans l₁ l₂ l₃ :
      PermutationA l₁ l₂ -> PermutationA l₂ l₃ -> PermutationA l₁ l₃.
-Local Hint Constructors PermutationA.
+Local Hint Constructors PermutationA : core.
 
 Global Instance: Equivalence PermutationA.
 Proof.
diff --git a/theories/Logic/JMeq.v b/theories/Logic/JMeq.v
index 25b7811417..3914f44a2c 100644
--- a/theories/Logic/JMeq.v
+++ b/theories/Logic/JMeq.v
@@ -31,7 +31,7 @@ Arguments JMeq_refl {A x} , [A] x.
 Register JMeq as core.JMeq.type.
 Register JMeq_refl as core.JMeq.refl.
 
-Hint Resolve JMeq_refl.
+Hint Resolve JMeq_refl : core.
 
 Definition JMeq_hom {A : Type} (x y : A) := JMeq x y.
 
@@ -42,7 +42,7 @@ Proof.
 intros; destruct H; trivial.
 Qed.
 
-Hint Immediate JMeq_sym.
+Hint Immediate JMeq_sym : core.
 
 Register JMeq_sym as core.JMeq.sym.
 
diff --git a/theories/MSets/MSetAVL.v b/theories/MSets/MSetAVL.v
index aec88f93bf..ac2a143472 100644
--- a/theories/MSets/MSetAVL.v
+++ b/theories/MSets/MSetAVL.v
@@ -305,13 +305,13 @@ Include MSetGenTree.Props X I.
 
 (** Automation and dedicated tactics *)
 
-Local Hint Immediate MX.eq_sym.
-Local Hint Unfold In lt_tree gt_tree Ok.
-Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
-Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
-Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
-Local Hint Resolve elements_spec2.
+Local Hint Immediate MX.eq_sym : core.
+Local Hint Unfold In lt_tree gt_tree Ok : core.
+Local Hint Constructors InT bst : core.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core.
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
+Local Hint Resolve elements_spec2 : core.
 
 (* Sometimes functional induction will expose too much of
    a tree structure. The following tactic allows factoring back
@@ -496,7 +496,7 @@ Proof.
   specialize (L m); rewrite remove_min_spec, e0 in L; simpl in L;
    [setoid_replace y with x|inv]; eauto.
 Qed.
-Local Hint Resolve remove_min_gt_tree.
+Local Hint Resolve remove_min_gt_tree : core.
 
 
 (** ** Merging two trees *)
diff --git a/theories/MSets/MSetGenTree.v b/theories/MSets/MSetGenTree.v
index 95868861fa..888f9850c1 100644
--- a/theories/MSets/MSetGenTree.v
+++ b/theories/MSets/MSetGenTree.v
@@ -46,7 +46,7 @@ End InfoTyp.
 Module Type Ops (X:OrderedType)(Info:InfoTyp).
 
 Definition elt := X.t.
-Hint Transparent elt.
+Hint Transparent elt : core.
 
 Inductive tree  : Type :=
 | Leaf : tree
@@ -342,11 +342,11 @@ Module Import MX := OrderedTypeFacts X.
 Scheme tree_ind := Induction for tree Sort Prop.
 Scheme bst_ind := Induction for bst Sort Prop.
 
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
-Local Hint Immediate MX.eq_sym.
-Local Hint Unfold In lt_tree gt_tree.
-Local Hint Constructors InT bst.
-Local Hint Unfold Ok.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core.
+Local Hint Immediate MX.eq_sym : core.
+Local Hint Unfold In lt_tree gt_tree : core.
+Local Hint Constructors InT bst : core.
+Local Hint Unfold Ok : core.
 
 (** Automatic treatment of [Ok] hypothesis *)
 
@@ -432,7 +432,7 @@ Lemma In_1 :
 Proof.
  induction s; simpl; intuition_in; eauto.
 Qed.
-Local Hint Immediate In_1.
+Local Hint Immediate In_1 : core.
 
 Instance In_compat : Proper (X.eq==>eq==>iff) InT.
 Proof.
@@ -478,7 +478,7 @@ Proof.
  unfold gt_tree; intuition_in; order.
 Qed.
 
-Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
 
 Lemma lt_tree_not_in :
  forall (x : elt) (t : tree), lt_tree x t -> ~ InT x t.
@@ -516,7 +516,7 @@ Proof.
  intros x x' Hx s s' Hs H y Hy. subst. setoid_rewrite <- Hx; auto.
 Qed.
 
-Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
 
 Ltac induct s x :=
  induction s as [|i l IHl x' r IHr]; simpl; intros;
@@ -699,7 +699,7 @@ Proof.
  intros; unfold elements; apply elements_spec2'; auto.
  intros; inversion H0.
 Qed.
-Local Hint Resolve elements_spec2.
+Local Hint Resolve elements_spec2 : core.
 
 Lemma elements_spec2w : forall s `(Ok s), NoDupA X.eq (elements s).
 Proof.
@@ -1035,7 +1035,7 @@ Qed.
 
 Definition Cmp c x y := CompSpec L.eq L.lt x y c.
 
-Local Hint Unfold Cmp flip.
+Local Hint Unfold Cmp flip : core.
 
 Lemma compare_end_Cmp :
  forall e2, Cmp (compare_end e2) nil (flatten_e e2).
diff --git a/theories/MSets/MSetInterface.v b/theories/MSets/MSetInterface.v
index f0e757157d..a4bbaef52d 100644
--- a/theories/MSets/MSetInterface.v
+++ b/theories/MSets/MSetInterface.v
@@ -884,10 +884,10 @@ Module MakeListOrdering (O:OrderedType).
         O.lt x y -> lt_list (x :: s) (y :: s')
     | lt_cons_eq : forall x y s s',
         O.eq x y -> lt_list s s' -> lt_list (x :: s) (y :: s').
- Hint Constructors lt_list.
+ Hint Constructors lt_list : core.
 
  Definition lt := lt_list.
- Hint Unfold lt.
+ Hint Unfold lt : core.
 
  Instance lt_strorder : StrictOrder lt.
  Proof.
@@ -933,13 +933,13 @@ Module MakeListOrdering (O:OrderedType).
   left; MO.order. right; rewrite <- E12; auto.
   left; MO.order. right; rewrite E12; auto.
  Qed.
- Hint Resolve eq_cons.
+ Hint Resolve eq_cons : core.
 
  Lemma cons_CompSpec : forall c x1 x2 l1 l2, O.eq x1 x2 ->
   CompSpec eq lt l1 l2 c -> CompSpec eq lt (x1::l1) (x2::l2) c.
  Proof.
   destruct c; simpl; inversion_clear 2; auto with relations.
  Qed.
- Hint Resolve cons_CompSpec.
+ Hint Resolve cons_CompSpec : core.
 
 End MakeListOrdering.
diff --git a/theories/MSets/MSetList.v b/theories/MSets/MSetList.v
index 35fe4cee4e..7b64818b24 100644
--- a/theories/MSets/MSetList.v
+++ b/theories/MSets/MSetList.v
@@ -231,14 +231,14 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Notation In := (InA X.eq).
 
   Existing Instance X.eq_equiv.
-  Hint Extern 20 => solve [order].
+  Hint Extern 20 => solve [order] : core.
 
   Definition IsOk s := Sort s.
 
   Class Ok (s:t) : Prop := ok : Sort s.
 
-  Hint Resolve ok.
-  Hint Unfold Ok.
+  Hint Resolve ok : core.
+  Hint Unfold Ok : core.
 
   Instance Sort_Ok s `(Hs : Sort s) : Ok s := { ok := Hs }.
 
@@ -276,7 +276,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
     destruct H; constructor; tauto.
   Qed.
 
-  Hint Extern 1 (Ok _) => rewrite <- isok_iff.
+  Hint Extern 1 (Ok _) => rewrite <- isok_iff : core.
 
   Ltac inv_ok := match goal with
    | H:sort X.lt (_ :: _) |- _ => inversion_clear H; inv_ok
@@ -326,7 +326,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intuition.
   intros; elim_compare x a; inv; intuition.
   Qed.
-  Hint Resolve add_inf.
+  Hint Resolve add_inf : core.
 
   Global Instance add_ok s x : forall `(Ok s), Ok (add x s).
   Proof.
@@ -353,7 +353,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   intros; elim_compare x a; inv; auto.
   apply Inf_lt with a; auto.
   Qed.
-  Hint Resolve remove_inf.
+  Hint Resolve remove_inf : core.
 
   Global Instance remove_ok s x : forall `(Ok s), Ok (remove x s).
   Proof.
@@ -396,7 +396,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   Proof.
   induction2.
   Qed.
-  Hint Resolve union_inf.
+  Hint Resolve union_inf : core.
 
   Global Instance union_ok s s' : forall `(Ok s, Ok s'), Ok (union s s').
   Proof.
@@ -422,7 +422,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
-  Hint Resolve inter_inf.
+  Hint Resolve inter_inf : core.
 
   Global Instance inter_ok s s' : forall `(Ok s, Ok s'), Ok (inter s s').
   Proof.
@@ -452,7 +452,7 @@ Module MakeRaw (X: OrderedType) <: RawSets X.
   apply Hrec'; auto.
   apply Inf_lt with x'; auto.
   Qed.
-  Hint Resolve diff_inf.
+  Hint Resolve diff_inf : core.
 
   Global Instance diff_ok s s' : forall `(Ok s, Ok s'), Ok (diff s s').
   Proof.
diff --git a/theories/MSets/MSetProperties.v b/theories/MSets/MSetProperties.v
index 3c7dea736b..29e57ff0a2 100644
--- a/theories/MSets/MSetProperties.v
+++ b/theories/MSets/MSetProperties.v
@@ -21,7 +21,7 @@ Require Import DecidableTypeEx OrdersLists MSetFacts MSetDecide.
 Set Implicit Arguments.
 Unset Strict Implicit.
 
-Hint Unfold transpose.
+Hint Unfold transpose : core.
 
 (** First, a functor for Weak Sets in functorial version. *)
 
@@ -735,7 +735,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   Proof.
   intros; rewrite cardinal_Empty; auto.
   Qed.
-  Hint Resolve cardinal_inv_1.
+  Hint Resolve cardinal_inv_1 : core.
 
   Lemma cardinal_inv_2 :
    forall s n, cardinal s = S n -> { x : elt | In x s }.
@@ -774,7 +774,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   exact Equal_cardinal.
   Qed.
 
-  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal.
+  Hint Resolve Add_add Add_remove Equal_remove cardinal_inv_1 Equal_cardinal : core.
 
   (** ** Cardinal and set operators *)
 
@@ -898,7 +898,7 @@ Module WPropertiesOn (Import E : DecidableType)(M : WSetsOn E).
   auto with set.
   Qed.
 
-  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2.
+  Hint Resolve subset_cardinal union_cardinal add_cardinal_1 add_cardinal_2 : core.
 
 End WPropertiesOn.
 
@@ -922,7 +922,7 @@ Module OrdProperties (M:Sets).
   Import M.E.
   Import M.
 
-  Hint Resolve elements_spec2.
+  Hint Resolve elements_spec2 : core.
   Hint Immediate
     min_elt_spec1 min_elt_spec2 min_elt_spec3
     max_elt_spec1 max_elt_spec2 max_elt_spec3 : set.
@@ -961,7 +961,7 @@ Module OrdProperties (M:Sets).
   Proof.
    intros a b H; unfold leb. rewrite H; auto.
   Qed.
-  Hint Resolve gtb_compat leb_compat.
+  Hint Resolve gtb_compat leb_compat : core.
 
   Lemma elements_split : forall x s,
    elements s = elements_lt x s ++ elements_ge x s.
diff --git a/theories/MSets/MSetRBT.v b/theories/MSets/MSetRBT.v
index eab01a55b0..f9105fdf74 100644
--- a/theories/MSets/MSetRBT.v
+++ b/theories/MSets/MSetRBT.v
@@ -450,13 +450,13 @@ Include MSetGenTree.Props X Color.
 Local Notation Rd := (Node Red).
 Local Notation Bk := (Node Black).
 
-Local Hint Immediate MX.eq_sym.
-Local Hint Unfold In lt_tree gt_tree Ok.
-Local Hint Constructors InT bst.
-Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok.
-Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node.
-Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans.
-Local Hint Resolve elements_spec2.
+Local Hint Immediate MX.eq_sym : core.
+Local Hint Unfold In lt_tree gt_tree Ok : core.
+Local Hint Constructors InT bst : core.
+Local Hint Resolve MX.eq_refl MX.eq_trans MX.lt_trans ok : core.
+Local Hint Resolve lt_leaf gt_leaf lt_tree_node gt_tree_node : core.
+Local Hint Resolve lt_tree_not_in lt_tree_trans gt_tree_not_in gt_tree_trans : core.
+Local Hint Resolve elements_spec2 : core.
 
 (** ** Singleton set *)
 
@@ -1136,7 +1136,7 @@ Record INV l1 l2 acc : Prop := {
  acc_sorted : sort X.lt acc;
  l1_lt_acc x y : InA X.eq x l1 -> InA X.eq y acc -> X.lt x y;
  l2_lt_acc x y : InA X.eq x l2 -> InA X.eq y acc -> X.lt x y}.
-Local Hint Resolve l1_sorted l2_sorted acc_sorted.
+Local Hint Resolve l1_sorted l2_sorted acc_sorted : core.
 
 Lemma INV_init s1 s2 `(Ok s1, Ok s2) :
  INV (rev_elements s1) (rev_elements s2) nil.
@@ -1506,8 +1506,8 @@ Class Rbt (t:tree) :=  RBT : exists d, rbt d t.
 (** ** Basic tactics and results about red-black *)
 
 Scheme rbt_ind := Induction for rbt Sort Prop.
-Local Hint Constructors rbt rrt arbt.
-Local Hint Extern 0 (notred _) => (exact I).
+Local Hint Constructors rbt rrt arbt : core.
+Local Hint Extern 0 (notred _) => (exact I) : core.
 Ltac invrb := intros; invtree rrt; invtree rbt; try contradiction.
 Ltac desarb := match goal with H:arbt _ _ |- _ => destruct H end.
 Ltac nonzero n := destruct n as [|n]; [try split; invrb|].
@@ -1519,7 +1519,7 @@ Proof.
  destruct l, r; descolor; invrb; auto.
 Qed.
 
-Local Hint Resolve rr_nrr_rb.
+Local Hint Resolve rr_nrr_rb : core.
 
 Lemma arb_nrr_rb n t :
  arbt n t -> notredred t -> rbt n t.
@@ -1533,7 +1533,7 @@ Proof.
  destruct 1; destruct t; descolor; invrb; auto.
 Qed.
 
-Local Hint Resolve arb_nrr_rb arb_nr_rb.
+Local Hint Resolve arb_nrr_rb arb_nr_rb : core.
 
 (** ** A Red-Black tree has indeed a logarithmic depth *)
 
diff --git a/theories/MSets/MSetWeakList.v b/theories/MSets/MSetWeakList.v
index 8df1ff1cdb..19058a767e 100644
--- a/theories/MSets/MSetWeakList.v
+++ b/theories/MSets/MSetWeakList.v
@@ -123,15 +123,15 @@ Module MakeRaw (X:DecidableType) <: WRawSets X.
   Let eqr:= (@Equivalence_Reflexive _ _ X.eq_equiv).
   Let eqsym:= (@Equivalence_Symmetric _ _ X.eq_equiv).
   Let eqtrans:= (@Equivalence_Transitive _ _ X.eq_equiv).
-  Hint Resolve eqr eqtrans.
-  Hint Immediate eqsym.
+  Hint Resolve eqr eqtrans : core.
+  Hint Immediate eqsym : core.
 
   Definition IsOk := NoDup.
 
   Class Ok (s:t) : Prop := ok : NoDup s.
 
-  Hint Unfold Ok.
-  Hint Resolve ok.
+  Hint Unfold Ok : core.
+  Hint Resolve ok : core.
 
   Instance NoDup_Ok s (nd : NoDup s) : Ok s := { ok := nd }.
 
diff --git a/theories/Numbers/Cyclic/ZModulo/ZModulo.v b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
index 784e81758c..4bcd22543f 100644
--- a/theories/Numbers/Cyclic/ZModulo/ZModulo.v
+++ b/theories/Numbers/Cyclic/ZModulo/ZModulo.v
@@ -60,7 +60,7 @@ Section ZModulo.
   apply Z.lt_gt.
   unfold wB, base; auto with zarith.
  Qed.
- Hint Resolve wB_pos.
+ Hint Resolve wB_pos : core.
 
  Lemma spec_to_Z_1 : forall x, 0 <= [|x|].
  Proof.
@@ -71,7 +71,7 @@ Section ZModulo.
  Proof.
   unfold to_Z; intros; destruct (Z_mod_lt x wB wB_pos); auto.
  Qed.
- Hint Resolve spec_to_Z_1 spec_to_Z_2.
+ Hint Resolve spec_to_Z_1 spec_to_Z_2 : core.
 
  Lemma spec_to_Z : forall x, 0 <= [|x|] < wB.
  Proof.
@@ -732,7 +732,7 @@ Section ZModulo.
  Proof.
  induction p; simpl; auto with zarith.
  Qed.
- Hint Resolve Ptail_pos.
+ Hint Resolve Ptail_pos : core.
 
  Lemma Ptail_bounded : forall p d, Zpos p < 2^(Zpos d) -> Ptail p < Zpos d.
  Proof.
diff --git a/theories/Numbers/Natural/Abstract/NDefOps.v b/theories/Numbers/Natural/Abstract/NDefOps.v
index 8e1be0d702..4539dea276 100644
--- a/theories/Numbers/Natural/Abstract/NDefOps.v
+++ b/theories/Numbers/Natural/Abstract/NDefOps.v
@@ -383,7 +383,7 @@ f_equiv. apply E, half_decrease.
 rewrite two_succ, <- not_true_iff_false, ltb_lt, nlt_ge, le_succ_l in H.
 order'.
 Qed.
-Hint Resolve log_good_step.
+Hint Resolve log_good_step : core.
 
 Theorem log_init : forall n, n < 2 -> log n == 0.
 Proof.
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v
index c2316689fc..d86112abc0 100644
--- a/theories/Program/Basics.v
+++ b/theories/Program/Basics.v
@@ -26,7 +26,7 @@ Arguments id {A} x.
 Definition compose {A B C} (g : B -> C) (f : A -> B) :=
   fun x : A => g (f x).
 
-Hint Unfold compose.
+Hint Unfold compose : core.
 
 Declare Scope program_scope.
 
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v
index 8479b9a2bb..f9d23e3cf6 100644
--- a/theories/Program/Wf.v
+++ b/theories/Program/Wf.v
@@ -110,7 +110,7 @@ Section Measure_well_founded.
 
 End Measure_well_founded.
 
-Hint Resolve measure_wf.
+Hint Resolve measure_wf : core.
 
 Section Fix_rects.
 
diff --git a/theories/QArith/Qcanon.v b/theories/QArith/Qcanon.v
index 81c318138e..f18fca99a0 100644
--- a/theories/QArith/Qcanon.v
+++ b/theories/QArith/Qcanon.v
@@ -66,7 +66,7 @@ Proof.
   rewrite hq, hq' in H'. subst q'. f_equal.
   apply eq_proofs_unicity. intros.  repeat decide equality.
 Qed.
-Hint Resolve Qc_is_canon.
+Hint Resolve Qc_is_canon : core.
 
 Theorem Qc_decomp: forall q q': Qc, (q:Q) = q' -> q = q'.
 Proof.
diff --git a/theories/QArith/Qreals.v b/theories/QArith/Qreals.v
index c832962590..b4c869b4dd 100644
--- a/theories/QArith/Qreals.v
+++ b/theories/QArith/Qreals.v
@@ -21,7 +21,7 @@ intros.
 now apply not_O_IZR.
 Qed.
 
-Hint Resolve IZR_nz Rmult_integral_contrapositive.
+Hint Resolve IZR_nz Rmult_integral_contrapositive : core.
 
 Lemma eqR_Qeq : forall x y : Q, Q2R x = Q2R y -> x==y.
 Proof.
diff --git a/theories/Reals/RIneq.v b/theories/Reals/RIneq.v
index 59a1049654..ec283b886e 100644
--- a/theories/Reals/RIneq.v
+++ b/theories/Reals/RIneq.v
@@ -1087,7 +1087,7 @@ Proof.
   replace (r2 + r1 + - r2) with r1 by ring.
   exact H.
 Qed.
-Hint Resolve Ropp_gt_lt_contravar.
+Hint Resolve Ropp_gt_lt_contravar : core.
 
 Lemma Ropp_lt_gt_contravar : forall r1 r2, r1 < r2 -> - r1 > - r2.
 Proof.
@@ -1204,7 +1204,7 @@ Lemma Rmult_lt_compat_r : forall r r1 r2, 0 < r -> r1 < r2 -> r1 * r < r2 * r.
 Proof.
   intros; rewrite (Rmult_comm r1 r); rewrite (Rmult_comm r2 r); auto with real.
 Qed.
-Hint Resolve Rmult_lt_compat_r.
+Hint Resolve Rmult_lt_compat_r : core.
 
 Lemma Rmult_gt_compat_r : forall r r1 r2, r > 0 -> r1 > r2 -> r1 * r > r2 * r.
 Proof. eauto using Rmult_lt_compat_r with rorders. Qed.
diff --git a/theories/Sets/Cpo.v b/theories/Sets/Cpo.v
index 3977097e8c..61fe55770b 100644
--- a/theories/Sets/Cpo.v
+++ b/theories/Sets/Cpo.v
@@ -95,7 +95,7 @@ End Bounds.
 Hint Resolve Totally_ordered_definition Upper_Bound_definition
   Lower_Bound_definition Lub_definition Glb_definition Bottom_definition
   Definition_of_Complete Definition_of_Complete
-  Definition_of_Conditionally_complete.
+  Definition_of_Conditionally_complete : core.
 
 Section Specific_orders.
   Variable U : Type.
diff --git a/theories/Sets/Infinite_sets.v b/theories/Sets/Infinite_sets.v
index bdeeb6a7c7..a0271a88a3 100644
--- a/theories/Sets/Infinite_sets.v
+++ b/theories/Sets/Infinite_sets.v
@@ -46,7 +46,7 @@ Section Approx.
     Defn_of_Approximant : Finite U X -> Included U X A -> Approximant A X.
 End Approx.
 
-Hint Resolve Defn_of_Approximant.
+Hint Resolve Defn_of_Approximant : core.
 
 Section Infinite_sets.
   Variable U : Type.
diff --git a/theories/Sets/Powerset.v b/theories/Sets/Powerset.v
index 88bcd6555c..50a7e401f8 100644
--- a/theories/Sets/Powerset.v
+++ b/theories/Sets/Powerset.v
@@ -38,43 +38,43 @@ Variable U : Type.
 Inductive Power_set (A:Ensemble U) : Ensemble (Ensemble U) :=
     Definition_of_Power_set :
       forall X:Ensemble U, Included U X A -> In (Ensemble U) (Power_set A) X.
-Hint Resolve Definition_of_Power_set.
+Hint Resolve Definition_of_Power_set : core.
 
 Theorem Empty_set_minimal : forall X:Ensemble U, Included U (Empty_set U) X.
 intro X; red.
 intros x H'; elim H'.
 Qed.
-Hint Resolve Empty_set_minimal.
+Hint Resolve Empty_set_minimal : core.
 
 Theorem Power_set_Inhabited :
  forall X:Ensemble U, Inhabited (Ensemble U) (Power_set X).
 intro X.
 apply Inhabited_intro with (Empty_set U); auto with sets.
 Qed.
-Hint Resolve Power_set_Inhabited.
+Hint Resolve Power_set_Inhabited : core.
 
 Theorem Inclusion_is_an_order : Order (Ensemble U) (Included U).
 auto 6 with sets.
 Qed.
-Hint Resolve Inclusion_is_an_order.
+Hint Resolve Inclusion_is_an_order : core.
 
 Theorem Inclusion_is_transitive : Transitive (Ensemble U) (Included U).
 elim Inclusion_is_an_order; auto with sets.
 Qed.
-Hint Resolve Inclusion_is_transitive.
+Hint Resolve Inclusion_is_transitive : core.
 
 Definition Power_set_PO : Ensemble U -> PO (Ensemble U).
 intro A; try assumption.
 apply Definition_of_PO with (Power_set A) (Included U); auto with sets.
 Defined.
-Hint Unfold Power_set_PO.
+Hint Unfold Power_set_PO : core.
 
 Theorem Strict_Rel_is_Strict_Included :
  same_relation (Ensemble U) (Strict_Included U)
    (Strict_Rel_of (Ensemble U) (Power_set_PO (Full_set U))).
 auto with sets.
 Qed.
-Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included.
+Hint Resolve Strict_Rel_Transitive Strict_Rel_is_Strict_Included : core.
 
 Lemma Strict_inclusion_is_transitive_with_inclusion :
  forall x y z:Ensemble U,
@@ -109,7 +109,7 @@ Theorem Empty_set_is_Bottom :
  forall A:Ensemble U, Bottom (Ensemble U) (Power_set_PO A) (Empty_set U).
 intro A; apply Bottom_definition; simpl; auto with sets.
 Qed.
-Hint Resolve Empty_set_is_Bottom.
+Hint Resolve Empty_set_is_Bottom : core.
 
 Theorem Union_minimal :
  forall a b X:Ensemble U,
@@ -117,7 +117,7 @@ Theorem Union_minimal :
 intros a b X H' H'0; red.
 intros x H'1; elim H'1; auto with sets.
 Qed.
-Hint Resolve Union_minimal.
+Hint Resolve Union_minimal : core.
 
 Theorem Intersection_maximal :
  forall a b X:Ensemble U,
@@ -145,7 +145,7 @@ intros a b; red.
 intros x H'; elim H'; auto with sets.
 Qed.
 Hint Resolve Union_increases_l Union_increases_r Intersection_decreases_l
-  Intersection_decreases_r.
+  Intersection_decreases_r : core.
 
 Theorem Union_is_Lub :
  forall A a b:Ensemble U,
diff --git a/theories/Sets/Relations_1_facts.v b/theories/Sets/Relations_1_facts.v
index 296ec42add..d275487e15 100644
--- a/theories/Sets/Relations_1_facts.v
+++ b/theories/Sets/Relations_1_facts.v
@@ -52,7 +52,7 @@ intros x y z h; elim h; intros H'3 H'4; clear h.
 intro h; elim h; intros H'5 H'6; clear h.
 split; apply H'1 with y; auto 10 with sets.
 Qed.
-Hint Resolve Equiv_from_preorder.
+Hint Resolve Equiv_from_preorder : core.
 
 Theorem Equiv_from_order :
  forall (U:Type) (R:Relation U),
@@ -60,21 +60,21 @@ Theorem Equiv_from_order :
 Proof.
 intros U R H'; elim H'; auto 10 with sets.
 Qed.
-Hint Resolve Equiv_from_order.
+Hint Resolve Equiv_from_order : core.
 
 Theorem contains_is_preorder :
  forall U:Type, Preorder (Relation U) (contains U).
 Proof.
 auto 10 with sets.
 Qed.
-Hint Resolve contains_is_preorder.
+Hint Resolve contains_is_preorder : core.
 
 Theorem same_relation_is_equivalence :
  forall U:Type, Equivalence (Relation U) (same_relation U).
 Proof.
 unfold same_relation at 1; auto 10 with sets.
 Qed.
-Hint Resolve same_relation_is_equivalence.
+Hint Resolve same_relation_is_equivalence : core.
 
 Theorem cong_reflexive_same_relation :
  forall (U:Type) (R R':Relation U),
diff --git a/theories/Sets/Relations_3_facts.v b/theories/Sets/Relations_3_facts.v
index 0c1f670d0e..18ea019526 100644
--- a/theories/Sets/Relations_3_facts.v
+++ b/theories/Sets/Relations_3_facts.v
@@ -38,7 +38,7 @@ Proof.
 intros U R x y H'; red.
 exists y; auto with sets.
 Qed.
-Hint Resolve Rstar_imp_coherent.
+Hint Resolve Rstar_imp_coherent : core.
 
 Theorem coherent_symmetric :
  forall (U:Type) (R:Relation U), Symmetric U (coherent U R).
diff --git a/theories/Sets/Uniset.v b/theories/Sets/Uniset.v
index 7940bda1a7..0ff304ed6b 100644
--- a/theories/Sets/Uniset.v
+++ b/theories/Sets/Uniset.v
@@ -41,21 +41,21 @@ Definition Singleton (a:A) :=
        end).
 
 Definition In (s:uniset) (a:A) : Prop := charac s a = true.
-Hint Unfold In.
+Hint Unfold In : core.
 
 (** uniset inclusion *)
 Definition incl (s1 s2:uniset) := forall a:A, leb (charac s1 a) (charac s2 a).
-Hint Unfold incl.
+Hint Unfold incl : core.
 
 (** uniset equality *)
 Definition seq (s1 s2:uniset) := forall a:A, charac s1 a = charac s2 a.
-Hint Unfold seq.
+Hint Unfold seq : core.
 
 Lemma leb_refl : forall b:bool, leb b b.
 Proof.
 destruct b; simpl; auto.
 Qed.
-Hint Resolve leb_refl.
+Hint Resolve leb_refl : core.
 
 Lemma incl_left : forall s1 s2:uniset, seq s1 s2 -> incl s1 s2.
 Proof.
@@ -71,7 +71,7 @@ Lemma seq_refl : forall x:uniset, seq x x.
 Proof.
 destruct x; unfold seq; auto.
 Qed.
-Hint Resolve seq_refl.
+Hint Resolve seq_refl : core.
 
 Lemma seq_trans : forall x y z:uniset, seq x y -> seq y z -> seq x z.
 Proof.
@@ -94,21 +94,21 @@ Lemma union_empty_left : forall x:uniset, seq x (union Emptyset x).
 Proof.
 unfold seq; unfold union; simpl; auto.
 Qed.
-Hint Resolve union_empty_left.
+Hint Resolve union_empty_left : core.
 
 Lemma union_empty_right : forall x:uniset, seq x (union x Emptyset).
 Proof.
 unfold seq; unfold union; simpl.
 intros x a; rewrite (orb_b_false (charac x a)); auto.
 Qed.
-Hint Resolve union_empty_right.
+Hint Resolve union_empty_right : core.
 
 Lemma union_comm : forall x y:uniset, seq (union x y) (union y x).
 Proof.
 unfold seq; unfold charac; unfold union.
 destruct x; destruct y; auto with bool.
 Qed.
-Hint Resolve union_comm.
+Hint Resolve union_comm : core.
 
 Lemma union_ass :
  forall x y z:uniset, seq (union (union x y) z) (union x (union y z)).
@@ -116,7 +116,7 @@ Proof.
 unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z; auto with bool.
 Qed.
-Hint Resolve union_ass.
+Hint Resolve union_ass : core.
 
 Lemma seq_left : forall x y z:uniset, seq x y -> seq (union x z) (union y z).
 Proof.
@@ -124,7 +124,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
-Hint Resolve seq_left.
+Hint Resolve seq_left : core.
 
 Lemma seq_right : forall x y z:uniset, seq x y -> seq (union z x) (union z y).
 Proof.
@@ -132,7 +132,7 @@ unfold seq; unfold union; unfold charac.
 destruct x; destruct y; destruct z.
 intros; elim H; auto.
 Qed.
-Hint Resolve seq_right.
+Hint Resolve seq_right : core.
 
 
 (** All the proofs that follow duplicate [Multiset_of_A] *)
diff --git a/theories/Sorting/Heap.v b/theories/Sorting/Heap.v
index 2ef162be4e..6a22501afa 100644
--- a/theories/Sorting/Heap.v
+++ b/theories/Sorting/Heap.v
@@ -36,8 +36,8 @@ Section defs.
   Hypothesis leA_trans : forall x y z:A, leA x y -> leA y z -> leA x z.
   Hypothesis leA_antisym : forall x y:A, leA x y -> leA y x -> eqA x y.
 
-  Hint Resolve leA_refl.
-  Hint Immediate eqA_dec leA_dec leA_antisym.
+  Hint Resolve leA_refl : core.
+  Hint Immediate eqA_dec leA_dec leA_antisym : core.
 
   Let emptyBag := EmptyBag A.
   Let singletonBag := SingletonBag _ eqA_dec.
diff --git a/theories/Sorting/Permutation.v b/theories/Sorting/Permutation.v
index 7b99b3626f..f5bc9eee4e 100644
--- a/theories/Sorting/Permutation.v
+++ b/theories/Sorting/Permutation.v
@@ -31,7 +31,7 @@ Inductive Permutation : list A -> list A -> Prop :=
 | perm_trans l l' l'' :
     Permutation l l' -> Permutation l' l'' -> Permutation l l''.
 
-Local Hint Constructors Permutation.
+Local Hint Constructors Permutation : core.
 
 (** Some facts about [Permutation] *)
 
@@ -71,13 +71,13 @@ Qed.
 
 End Permutation.
 
-Hint Resolve Permutation_refl perm_nil perm_skip.
+Hint Resolve Permutation_refl perm_nil perm_skip : core.
 
 (* These hints do not reduce the size of the problem to solve and they
    must be used with care to avoid combinatoric explosions *)
 
-Local Hint Resolve perm_swap perm_trans.
-Local Hint Resolve Permutation_sym Permutation_trans.
+Local Hint Resolve perm_swap perm_trans : core.
+Local Hint Resolve Permutation_sym Permutation_trans : core.
 
 (* This provides reflexivity, symmetry and transitivity and rewriting
    on morphims to come *)
@@ -156,7 +156,7 @@ Qed.
 Lemma Permutation_cons_append : forall (l : list A) x,
   Permutation (x :: l) (l ++ x :: nil).
 Proof. induction l; intros; auto. simpl. rewrite <- IHl; auto. Qed.
-Local Hint Resolve Permutation_cons_append.
+Local Hint Resolve Permutation_cons_append : core.
 
 Theorem Permutation_app_comm : forall (l l' : list A),
   Permutation (l ++ l') (l' ++ l).
@@ -166,7 +166,7 @@ Proof.
   rewrite app_comm_cons, Permutation_cons_append.
   now rewrite <- app_assoc.
 Qed.
-Local Hint Resolve Permutation_app_comm.
+Local Hint Resolve Permutation_app_comm : core.
 
 Theorem Permutation_cons_app : forall (l l1 l2:list A) a,
   Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2).
@@ -175,7 +175,7 @@ Proof.
   rewrite app_comm_cons, Permutation_cons_append.
   now rewrite <- app_assoc.
 Qed.
-Local Hint Resolve Permutation_cons_app.
+Local Hint Resolve Permutation_cons_app : core.
 
 Lemma Permutation_Add a l l' : Add a l l' -> Permutation (a::l) l'.
 Proof.
@@ -188,7 +188,7 @@ Theorem Permutation_middle : forall (l1 l2:list A) a,
 Proof.
   auto.
 Qed.
-Local Hint Resolve Permutation_middle.
+Local Hint Resolve Permutation_middle : core.
 
 Theorem Permutation_rev : forall (l : list A), Permutation l (rev l).
 Proof.
diff --git a/theories/Sorting/Sorted.v b/theories/Sorting/Sorted.v
index 89e9c7f3e1..6782dd9ca3 100644
--- a/theories/Sorting/Sorted.v
+++ b/theories/Sorting/Sorted.v
@@ -137,8 +137,8 @@ Section defs.
 
 End defs.
 
-Hint Constructors HdRel.
-Hint Constructors Sorted.
+Hint Constructors HdRel : core.
+Hint Constructors Sorted : core.
 
 (* begin hide *)
 (* Compatibility with deprecated file Sorting.v *)
diff --git a/theories/Structures/DecidableType.v b/theories/Structures/DecidableType.v
index 24333ad815..f82ca5fa3c 100644
--- a/theories/Structures/DecidableType.v
+++ b/theories/Structures/DecidableType.v
@@ -38,8 +38,8 @@ Module KeyDecidableType(D:DecidableType).
   Definition eqke (p p':key*elt) :=
           eq (fst p) (fst p') /\ (snd p) = (snd p').
 
-  Hint Unfold eqk eqke.
-  Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold eqk eqke : core.
+  Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
 
@@ -70,8 +70,8 @@ Module KeyDecidableType(D:DecidableType).
     unfold eqke; intuition; [ eauto | congruence ].
   Qed.
 
-  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
-  Hint Immediate eqk_sym eqke_sym.
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
   Proof. split; eauto. Qed.
@@ -84,7 +84,7 @@ Module KeyDecidableType(D:DecidableType).
   Proof.
     unfold eqke; induction 1; intuition. 
   Qed.
-  Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk : core.
 
   Lemma InA_eqk : forall p q m, eqk p q -> InA eqk p m -> InA eqk q m.
   Proof.
@@ -94,7 +94,7 @@ Module KeyDecidableType(D:DecidableType).
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
 
-  Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
 
@@ -140,13 +140,13 @@ Module KeyDecidableType(D:DecidableType).
 
  End Elt.
 
- Hint Unfold eqk eqke.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
- Hint Immediate eqk_sym eqke_sym.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Resolve In_inv_2 In_inv_3.
+ Hint Unfold eqk eqke : core.
+ Hint Extern 2 (eqke ?a ?b) => split : core.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ Hint Immediate eqk_sym eqke_sym : core.
+ Hint Resolve InA_eqke_eqk : core.
+ Hint Unfold MapsTo In : core.
+ Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyDecidableType.
 
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 *)
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.
 
diff --git a/theories/Structures/OrderedType.v b/theories/Structures/OrderedType.v
index f6fc247d5a..d000b75bf4 100644
--- a/theories/Structures/OrderedType.v
+++ b/theories/Structures/OrderedType.v
@@ -42,8 +42,8 @@ Module Type MiniOrderedType.
 
   Parameter compare : forall x y : t, Compare lt eq x y.
 
-  Hint Immediate eq_sym.
-  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+  Hint Immediate eq_sym : core.
+  Hint Resolve eq_refl eq_trans lt_not_eq lt_trans : core.
 
 End MiniOrderedType.
 
@@ -143,9 +143,9 @@ Module OrderedTypeFacts (Import O: OrderedType).
   Lemma eq_not_gt x y : eq x y -> ~ lt y x. Proof. order. Qed.
   Lemma lt_not_gt x y : lt x y -> ~ lt y x. Proof. order. Qed.
 
-  Hint Resolve gt_not_eq eq_not_lt.
-  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq.
-  Hint Resolve eq_not_gt lt_antirefl lt_not_gt.
+  Hint Resolve gt_not_eq eq_not_lt : core.
+  Hint Immediate eq_lt lt_eq le_eq eq_le neq_eq eq_neq : core.
+  Hint Resolve eq_not_gt lt_antirefl lt_not_gt : core.
 
   Lemma elim_compare_eq :
    forall x y : t,
@@ -247,8 +247,8 @@ Proof. exact (SortA_NoDupA eq_equiv lt_strorder lt_compat). Qed.
 
 End ForNotations.
 
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
+Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeFacts.
 
@@ -266,8 +266,8 @@ Module KeyOrderedType(O:OrderedType).
           eq (fst p) (fst p') /\ (snd p) = (snd p').
   Definition ltk (p p':key*elt) := lt (fst p) (fst p').
 
-  Hint Unfold eqk eqke ltk.
-  Hint Extern 2 (eqke ?a ?b) => split.
+  Hint Unfold eqk eqke ltk : core.
+  Hint Extern 2 (eqke ?a ?b) => split : core.
 
    (* eqke is stricter than eqk *)
 
@@ -283,7 +283,7 @@ Module KeyOrderedType(O:OrderedType).
 
    Lemma ltk_right_l : forall x k e e', ltk (k,e) x -> ltk (k,e') x.
    Proof. auto. Qed.
-   Hint Immediate ltk_right_r ltk_right_l.
+   Hint Immediate ltk_right_r ltk_right_l : core.
 
   (* eqk, eqke are equalities, ltk is a strict order *)
 
@@ -319,9 +319,9 @@ Module KeyOrderedType(O:OrderedType).
     exact (lt_not_eq H H1).
   Qed.
 
-  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
-  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
-  Hint Immediate eqk_sym eqke_sym.
+  Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+  Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core.
+  Hint Immediate eqk_sym eqke_sym : core.
 
   Global Instance eqk_equiv : Equivalence eqk.
   Proof. constructor; eauto. Qed.
@@ -359,22 +359,22 @@ Module KeyOrderedType(O:OrderedType).
       intros (k,e) (k',e') (k'',e'').
       unfold ltk, eqk; simpl; eauto.
   Qed.
-  Hint Resolve eqk_not_ltk.
-  Hint Immediate ltk_eqk eqk_ltk.
+  Hint Resolve eqk_not_ltk : core.
+  Hint Immediate ltk_eqk eqk_ltk : core.
 
   Lemma InA_eqke_eqk :
      forall x m, InA eqke x m -> InA eqk x m.
   Proof.
     unfold eqke; induction 1; intuition.
   Qed.
-  Hint Resolve InA_eqke_eqk.
+  Hint Resolve InA_eqke_eqk : core.
 
   Definition MapsTo (k:key)(e:elt):= InA eqke (k,e).
   Definition In k m := exists e:elt, MapsTo k e m.
   Notation Sort := (sort ltk).
   Notation Inf := (lelistA ltk).
 
-  Hint Unfold MapsTo In.
+  Hint Unfold MapsTo In : core.
 
   (* An alternative formulation for [In k l] is [exists e, InA eqk (k,e) l] *)
 
@@ -405,8 +405,8 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt : forall l x x', ltk x x' -> Inf x' l -> Inf x l.
   Proof. exact (InfA_ltA ltk_strorder). Qed.
 
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
+  Hint Immediate Inf_eq : core.
+  Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In :
       forall l p q, Sort l -> Inf q l -> InA eqk p l -> ltk q p.
@@ -469,19 +469,19 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
- Hint Unfold eqk eqke ltk.
- Hint Extern 2 (eqke ?a ?b) => split.
- Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl.
- Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke.
- Hint Immediate eqk_sym eqke_sym.
- Hint Resolve eqk_not_ltk.
- Hint Immediate ltk_eqk eqk_ltk.
- Hint Resolve InA_eqke_eqk.
- Hint Unfold MapsTo In.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
- Hint Resolve In_inv_2 In_inv_3.
+ Hint Unfold eqk eqke ltk : core.
+ Hint Extern 2 (eqke ?a ?b) => split : core.
+ Hint Resolve eqk_trans eqke_trans eqk_refl eqke_refl : core.
+ Hint Resolve ltk_trans ltk_not_eqk ltk_not_eqke : core.
+ Hint Immediate eqk_sym eqke_sym : core.
+ Hint Resolve eqk_not_ltk : core.
+ Hint Immediate ltk_eqk eqk_ltk : core.
+ Hint Resolve InA_eqke_eqk : core.
+ Hint Unfold MapsTo In : core.
+ Hint Immediate Inf_eq : core.
+ Hint Resolve Inf_lt : core.
+ Hint Resolve Sort_Inf_NotIn : core.
+ Hint Resolve In_inv_2 In_inv_3 : core.
 
 End KeyOrderedType.
 
diff --git a/theories/Structures/Orders.v b/theories/Structures/Orders.v
index 42756ad339..310a22a0a4 100644
--- a/theories/Structures/Orders.v
+++ b/theories/Structures/Orders.v
@@ -181,7 +181,7 @@ Module OTF_to_TotalOrder (O:OrderedTypeFull) <: TotalOrder
     we coerce [bool] into [Prop]. *)
 
 Local Coercion is_true : bool >-> Sortclass.
-Hint Unfold is_true.
+Hint Unfold is_true : core.
 
 Module Type HasLeb (Import T:Typ).
  Parameter Inline leb : t -> t -> bool.
diff --git a/theories/Structures/OrdersLists.v b/theories/Structures/OrdersLists.v
index abdb9eff05..fef9b14a9e 100644
--- a/theories/Structures/OrdersLists.v
+++ b/theories/Structures/OrdersLists.v
@@ -50,8 +50,8 @@ Proof. exact (InfA_alt O.eq_equiv O.lt_strorder O.lt_compat). Qed.
 Lemma Sort_NoDup : forall l, Sort l -> NoDup l.
 Proof. exact (SortA_NoDupA O.eq_equiv O.lt_strorder O.lt_compat) . Qed.
 
-Hint Resolve ListIn_In Sort_NoDup Inf_lt.
-Hint Immediate In_eq Inf_lt.
+Hint Resolve ListIn_In Sort_NoDup Inf_lt : core.
+Hint Immediate In_eq Inf_lt : core.
 
 End OrderedTypeLists.
 
@@ -66,7 +66,7 @@ Module KeyOrderedType(O:OrderedType).
 
  Definition ltk {elt} : relation (key*elt) := O.lt @@1.
 
- Hint Unfold ltk.
+ Hint Unfold ltk : core.
 
  (* ltk is a strict order *)
 
@@ -109,8 +109,8 @@ Module KeyOrderedType(O:OrderedType).
   Lemma Inf_lt l x x' : ltk x x' -> Inf x' l -> Inf x l.
   Proof. apply InfA_ltA; auto with *. Qed.
 
-  Hint Immediate Inf_eq.
-  Hint Resolve Inf_lt.
+  Hint Immediate Inf_eq : core.
+  Hint Resolve Inf_lt : core.
 
   Lemma Sort_Inf_In l p q : Sort l -> Inf q l -> InA eqk p l -> ltk q p.
   Proof. apply SortA_InfA_InA; auto with *. Qed.
@@ -148,10 +148,10 @@ Module KeyOrderedType(O:OrderedType).
 
  End Elt.
 
- Hint Resolve ltk_not_eqk ltk_not_eqke.
- Hint Immediate Inf_eq.
- Hint Resolve Inf_lt.
- Hint Resolve Sort_Inf_NotIn.
+ Hint Resolve ltk_not_eqk ltk_not_eqke : core.
+ Hint Immediate Inf_eq : core.
+ Hint Resolve Inf_lt : core.
+ Hint Resolve Sort_Inf_NotIn : core.
 
 End KeyOrderedType.
 
diff --git a/theories/Vectors/VectorDef.v b/theories/Vectors/VectorDef.v
index 4a2bddf35c..7f96aa6b87 100644
--- a/theories/Vectors/VectorDef.v
+++ b/theories/Vectors/VectorDef.v
@@ -269,28 +269,28 @@ Section SCANNING.
 Inductive Forall {A} (P: A -> Prop): forall {n} (v: t A n), Prop :=
  |Forall_nil: Forall P []
  |Forall_cons {n} x (v: t A n): P x -> Forall P v -> Forall P (x::v).
-Hint Constructors Forall.
+Hint Constructors Forall : core.
 
 Inductive Exists {A} (P:A->Prop): forall {n}, t A n -> Prop :=
  |Exists_cons_hd {m} x (v: t A m): P x -> Exists P (x::v)
  |Exists_cons_tl {m} x (v: t A m): Exists P v -> Exists P (x::v).
-Hint Constructors Exists.
+Hint Constructors Exists : core.
 
 Inductive In {A} (a:A): forall {n}, t A n -> Prop :=
  |In_cons_hd {m} (v: t A m): In a (a::v)
  |In_cons_tl {m} x (v: t A m): In a v -> In a (x::v).
-Hint Constructors In.
+Hint Constructors In : core.
 
 Inductive Forall2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Forall2_nil: Forall2 P [] []
  |Forall2_cons {m} x1 x2 (v1:t A m) v2: P x1 x2 -> Forall2 P v1 v2 ->
     Forall2 P (x1::v1) (x2::v2).
-Hint Constructors Forall2.
+Hint Constructors Forall2 : core.
 
 Inductive Exists2 {A B} (P:A->B->Prop): forall {n}, t A n -> t B n -> Prop :=
  |Exists2_cons_hd {m} x1 x2 (v1: t A m) (v2: t B m): P x1 x2 -> Exists2 P (x1::v1) (x2::v2)
  |Exists2_cons_tl {m} x1 x2 (v1:t A m) v2: Exists2 P v1 v2 -> Exists2 P (x1::v1) (x2::v2).
-Hint Constructors Exists2.
+Hint Constructors Exists2 : core.
 
 End SCANNING.
 
diff --git a/theories/Wellfounded/Inclusion.v b/theories/Wellfounded/Inclusion.v
index ff233ef9c6..18c4bedd9a 100644
--- a/theories/Wellfounded/Inclusion.v
+++ b/theories/Wellfounded/Inclusion.v
@@ -22,7 +22,7 @@ Section WfInclusion.
     apply Acc_intro; auto with sets.
   Qed.
 
-  Hint Resolve Acc_incl.
+  Hint Resolve Acc_incl : core.
 
   Theorem wf_incl : inclusion A R1 R2 -> well_founded R2 -> well_founded R1.
   Proof.
diff --git a/theories/Wellfounded/Transitive_Closure.v b/theories/Wellfounded/Transitive_Closure.v
index 59068623ae..0d56d88869 100644
--- a/theories/Wellfounded/Transitive_Closure.v
+++ b/theories/Wellfounded/Transitive_Closure.v
@@ -31,7 +31,7 @@ Section Wf_Transitive_Closure.
     apply Acc_inv with y; auto with sets.
   Defined.
 
-  Hint Resolve Acc_clos_trans.
+  Hint Resolve Acc_clos_trans : core.
 
   Lemma Acc_inv_trans : forall x y:A, trans_clos y x -> Acc R x -> Acc R y.
   Proof.
diff --git a/theories/ZArith/Zdiv.v b/theories/ZArith/Zdiv.v
index 74614e114a..c278cada61 100644
--- a/theories/ZArith/Zdiv.v
+++ b/theories/ZArith/Zdiv.v
@@ -73,7 +73,7 @@ Proof.
  intros; unfold Remainder, Remainder_alt; omega with *.
 Qed.
 
-Hint Unfold Remainder.
+Hint Unfold Remainder : core.
 
 (** Now comes the fully general result about Euclidean division. *)
 
diff --git a/theories/ZArith/Zlogarithm.v b/theories/ZArith/Zlogarithm.v
index 24412e9431..b8c7319939 100644
--- a/theories/ZArith/Zlogarithm.v
+++ b/theories/ZArith/Zlogarithm.v
@@ -47,7 +47,7 @@ Section Log_pos. (* Log of positive integers *)
       | xI n => Z.succ (Z.succ (log_inf n))	(* 2n+1 *)
     end.
 
-  Hint Unfold log_inf log_sup.
+ Hint Unfold log_inf log_sup : core.
 
   Lemma Psize_log_inf : forall p, Zpos (Pos.size p) = Z.succ (log_inf p).
   Proof.
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 08aee9533f..0405e4f27c 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1098,13 +1098,28 @@ let vernac_restore_state file =
 let vernac_create_hintdb ~module_local id b =
   Hints.create_hint_db module_local id full_transparent_state b
 
-let vernac_remove_hints ~module_local dbs ids =
-  Hints.remove_hints module_local dbs (List.map Smartlocate.global_with_alias ids)
+let warn_implicit_core_hint_db =
+  CWarnings.create ~name:"implicit-core-hint-db" ~category:"deprecated"
+         (fun () -> strbrk "Adding and removing hints in the core database implicitly is deprecated. "
+             ++ strbrk"Please specify a hint database.")
+
+let vernac_remove_hints ~module_local dbnames ids =
+  let dbnames =
+    if List.is_empty dbnames then
+      (warn_implicit_core_hint_db (); ["core"])
+    else dbnames
+  in
+  Hints.remove_hints module_local dbnames (List.map Smartlocate.global_with_alias ids)
 
-let vernac_hints ~atts lb h =
+let vernac_hints ~atts dbnames h =
+  let dbnames =
+    if List.is_empty dbnames then
+      (warn_implicit_core_hint_db (); ["core"])
+    else dbnames
+  in
   let local, poly = Attributes.(parse Notations.(locality ++ polymorphic) atts) in
   let local = enforce_module_locality local in
-  Hints.add_hints ~local lb (Hints.interp_hints poly h)
+  Hints.add_hints ~local dbnames (Hints.interp_hints poly h)
 
 let vernac_syntactic_definition ~module_local lid x y =
   Dumpglob.dump_definition lid false "syndef";