diff --git a/theories/base.v b/theories/base.v
index 7967f45e5d71ee54f86f62ef2b847dffd7227872..2a96208b4c52dfe13bd67337230a213fb0d86ff3 100644
--- a/theories/base.v
+++ b/theories/base.v
@@ -166,8 +166,8 @@ Notation "(≠@{ A } )" := (λ X Y, ¬X =@{A} Y) (only parsing) : stdpp_scope.
 Notation "X ≠@{ A } Y":= (¬X =@{ A } Y)
   (at level 70, only parsing, no associativity) : stdpp_scope.
 
-Hint Extern 0 (_ = _) => reflexivity.
-Hint Extern 100 (_ ≠ _) => discriminate.
+Hint Extern 0 (_ = _) => reflexivity : core.
+Hint Extern 100 (_ ≠ _) => discriminate : core.
 
 Instance: ∀ A, PreOrder (=@{A}).
 Proof. split; repeat intro; congruence. Qed.
@@ -234,8 +234,8 @@ Instance: Params (@equiv) 2.
 (for types that have an [Equiv] instance) rather than the standard Leibniz
 equality. *)
 Instance equiv_default_relation `{Equiv A} : DefaultRelation (≡) | 3.
-Hint Extern 0 (_ ≡ _) => reflexivity.
-Hint Extern 0 (_ ≡ _) => symmetry; assumption.
+Hint Extern 0 (_ ≡ _) => reflexivity : core.
+Hint Extern 0 (_ ≡ _) => symmetry; assumption : core.
 
 
 (** * Type classes *)
@@ -406,8 +406,8 @@ Notation "(↔)" := iff (only parsing) : stdpp_scope.
 Notation "( A ↔)" := (iff A) (only parsing) : stdpp_scope.
 Notation "(↔ B )" := (λ A, A ↔ B) (only parsing) : stdpp_scope.
 
-Hint Extern 0 (_ ↔ _) => reflexivity.
-Hint Extern 0 (_ ↔ _) => symmetry; assumption.
+Hint Extern 0 (_ ↔ _) => reflexivity : core.
+Hint Extern 0 (_ ↔ _) => symmetry; assumption : core.
 
 Lemma or_l P Q : ¬Q → P ∨ Q ↔ P.
 Proof. tauto. Qed.
@@ -539,9 +539,9 @@ Notation zip := (zip_with pair).
 (** ** Booleans *)
 (** The following coercion allows us to use Booleans as propositions. *)
 Coercion Is_true : bool >-> Sortclass.
-Hint Unfold Is_true.
-Hint Immediate Is_true_eq_left.
-Hint Resolve orb_prop_intro andb_prop_intro.
+Hint Unfold Is_true : core.
+Hint Immediate Is_true_eq_left : core.
+Hint Resolve orb_prop_intro andb_prop_intro : core.
 Notation "(&&)" := andb (only parsing).
 Notation "(||)" := orb (only parsing).
 Infix "&&*" := (zip_with (&&)) (at level 40).
@@ -826,9 +826,9 @@ Infix "⊆2*" := (Forall2 (λ p q, p.2 ⊆ q.2)) (at level 70) : stdpp_scope.
 Infix "⊆1**" := (Forall2 (λ p q, p.1 ⊆* q.1)) (at level 70) : stdpp_scope.
 Infix "⊆2**" := (Forall2 (λ p q, p.2 ⊆* q.2)) (at level 70) : stdpp_scope.
 
-Hint Extern 0 (_ ⊆ _) => reflexivity.
-Hint Extern 0 (_ ⊆* _) => reflexivity.
-Hint Extern 0 (_ ⊆** _) => reflexivity.
+Hint Extern 0 (_ ⊆ _) => reflexivity : core.
+Hint Extern 0 (_ ⊆* _) => reflexivity : core.
+Hint Extern 0 (_ ⊆** _) => reflexivity : core.
 
 Infix "⊂" := (strict (⊆)) (at level 70) : stdpp_scope.
 Notation "(⊂)" := (strict (⊆)) (only parsing) : stdpp_scope.
@@ -886,8 +886,8 @@ Infix "##1*" := (Forall2 (λ p q, p.1 ## q.1)) (at level 70) : stdpp_scope.
 Infix "##2*" := (Forall2 (λ p q, p.2 ## q.2)) (at level 70) : stdpp_scope.
 Infix "##1**" := (Forall2 (λ p q, p.1 ##* q.1)) (at level 70) : stdpp_scope.
 Infix "##2**" := (Forall2 (λ p q, p.2 ##* q.2)) (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ## _) => symmetry; eassumption.
-Hint Extern 0 (_ ##* _) => symmetry; eassumption.
+Hint Extern 0 (_ ## _) => symmetry; eassumption : core.
+Hint Extern 0 (_ ##* _) => symmetry; eassumption : core.
 
 Class DisjointE E A := disjointE : E → A → A → Prop.
 Hint Mode DisjointE - ! : typeclass_instances.
@@ -904,7 +904,7 @@ Notation "X ##{ Γ1 , Γ2 , .. , Γ3 } Y" := (disjoint (pair .. (Γ1, Γ2) .. Γ
 Notation "Xs ##{ Γ1 , Γ2 , .. , Γ3 }* Ys" :=
   (Forall2 (disjoint (pair .. (Γ1, Γ2) .. Γ3)) Xs Ys)
   (at level 70, format "Xs  ##{ Γ1 ,  Γ2 , .. , Γ3 }*  Ys") : stdpp_scope.
-Hint Extern 0 (_ ##{_} _) => symmetry; eassumption.
+Hint Extern 0 (_ ##{_} _) => symmetry; eassumption : core.
 
 Class DisjointList A := disjoint_list : list A → Prop.
 Hint Mode DisjointList ! : typeclass_instances.
@@ -1212,7 +1212,7 @@ Notation "(⊑@{ A } )" := (@sqsubseteq A _) (only parsing) : stdpp_scope.
 
 Instance sqsubseteq_rewrite `{SqSubsetEq A} : RewriteRelation (⊑).
 
-Hint Extern 0 (_ ⊑ _) => reflexivity.
+Hint Extern 0 (_ ⊑ _) => reflexivity : core.
 
 Class Meet A := meet: A → A → A.
 Hint Mode Meet ! : typeclass_instances.
diff --git a/theories/coPset.v b/theories/coPset.v
index fc5282e3cd06ad6bcf10aca07d0102c647815f05..6c45429d199bd6cba60f9ad9d28140428dd4585e 100644
--- a/theories/coPset.v
+++ b/theories/coPset.v
@@ -36,7 +36,7 @@ Lemma coPNode_wf_l b l r : coPset_wf (coPNode b l r) → coPset_wf l.
 Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
 Lemma coPNode_wf_r b l r : coPset_wf (coPNode b l r) → coPset_wf r.
 Proof. destruct b, l as [[]|],r as [[]|]; simpl; rewrite ?andb_True; tauto. Qed.
-Local Hint Immediate coPNode_wf_l coPNode_wf_r.
+Local Hint Immediate coPNode_wf_l coPNode_wf_r : core.
 
 Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
   match b, l, r with
@@ -47,7 +47,7 @@ Definition coPNode' (b : bool) (l r : coPset_raw) : coPset_raw :=
 Arguments coPNode' : simpl never.
 Lemma coPNode_wf b l r : coPset_wf l → coPset_wf r → coPset_wf (coPNode' b l r).
 Proof. destruct b, l as [[]|], r as [[]|]; simpl; auto. Qed.
-Hint Resolve coPNode_wf.
+Hint Resolve coPNode_wf : core.
 
 Fixpoint coPset_elem_of_raw (p : positive) (t : coPset_raw) {struct t} : bool :=
   match t, p with
@@ -207,7 +207,7 @@ Defined.
 (** * Top *)
 Lemma coPset_top_subseteq (X : coPset) : X ⊆ ⊤.
 Proof. done. Qed.
-Hint Resolve coPset_top_subseteq.
+Hint Resolve coPset_top_subseteq : core.
 
 (** * Finite sets *)
 Fixpoint coPset_finite (t : coPset_raw) : bool :=
diff --git a/theories/decidable.v b/theories/decidable.v
index cd2ad8d4a457d88635f2ffc9e3b79f546e2838de..1f51743866bb376973efa8cdc7b2c842c5797367 100644
--- a/theories/decidable.v
+++ b/theories/decidable.v
@@ -107,7 +107,7 @@ Lemma bool_decide_unpack (P : Prop) {dec : Decision P} : bool_decide P → P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
 Lemma bool_decide_pack (P : Prop) {dec : Decision P} : P → bool_decide P.
 Proof. rewrite bool_decide_spec; trivial. Qed.
-Hint Resolve bool_decide_pack.
+Hint Resolve bool_decide_pack : core.
 Lemma bool_decide_true (P : Prop) `{Decision P} : P → bool_decide P = true.
 Proof. case_bool_decide; tauto. Qed.
 Lemma bool_decide_false (P : Prop) `{Decision P} : ¬P → bool_decide P = false.
diff --git a/theories/fin_maps.v b/theories/fin_maps.v
index 7185a59fafaeac1ad9f0a7b0377fd19fc74019e6..7abefa2b5a7381489eb1236eda45aac6345b95bc 100644
--- a/theories/fin_maps.v
+++ b/theories/fin_maps.v
@@ -97,7 +97,7 @@ Definition map_included `{∀ A, Lookup K A (M A)} {A}
 Definition map_disjoint `{∀ A, Lookup K A (M A)} {A} : relation (M A) :=
   map_relation (λ _ _, False) (λ _, True) (λ _, True).
 Infix "##ₘ" := map_disjoint (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption.
+Hint Extern 0 (_ ##ₘ _) => symmetry; eassumption : core.
 Notation "( m ##ₘ.)" := (map_disjoint m) (only parsing) : stdpp_scope.
 Notation "(.##ₘ m )" := (λ m2, m2 ##ₘ m) (only parsing) : stdpp_scope.
 Instance map_subseteq `{∀ A, Lookup K A (M A)} {A} : SubsetEq (M A) :=
diff --git a/theories/gmultiset.v b/theories/gmultiset.v
index a7c9c1107b24f869c905fec8f4938863365612dd..71ab27658bd685b5ab185a8e26e8e133d560486f 100644
--- a/theories/gmultiset.v
+++ b/theories/gmultiset.v
@@ -261,7 +261,7 @@ Defined.
 
 Lemma gmultiset_subset_subseteq X Y : X ⊂ Y → X ⊆ Y.
 Proof. apply strict_include. Qed.
-Hint Resolve gmultiset_subset_subseteq.
+Hint Resolve gmultiset_subset_subseteq : core.
 
 Lemma gmultiset_empty_subseteq X : ∅ ⊆ X.
 Proof. intros x. rewrite multiplicity_empty. lia. Qed.
diff --git a/theories/list.v b/theories/list.v
index b74c1a138f7632dec36f8d1fed90fd12f4d31e72..219ea36c455d6ca1fd042ed560f2c6d25eeca334 100644
--- a/theories/list.v
+++ b/theories/list.v
@@ -246,8 +246,8 @@ Definition suffix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = k ++ l1.
 Definition prefix {A} : relation (list A) := λ l1 l2, ∃ k, l2 = l1 ++ k.
 Infix "`suffix_of`" := suffix (at level 70) : stdpp_scope.
 Infix "`prefix_of`" := prefix (at level 70) : stdpp_scope.
-Hint Extern 0 (_ `prefix_of` _) => reflexivity.
-Hint Extern 0 (_ `suffix_of` _) => reflexivity.
+Hint Extern 0 (_ `prefix_of` _) => reflexivity : core.
+Hint Extern 0 (_ `suffix_of` _) => reflexivity : core.
 
 Section prefix_suffix_ops.
   Context `{EqDecision A}.
@@ -276,7 +276,7 @@ Inductive sublist {A} : relation (list A) :=
   | sublist_skip x l1 l2 : sublist l1 l2 → sublist (x :: l1) (x :: l2)
   | sublist_cons x l1 l2 : sublist l1 l2 → sublist l1 (x :: l2).
 Infix "`sublist_of`" := sublist (at level 70) : stdpp_scope.
-Hint Extern 0 (_ `sublist_of` _) => reflexivity.
+Hint Extern 0 (_ `sublist_of` _) => reflexivity : core.
 
 (** A list [l2] submseteq a list [l1] if [l2] is obtained by removing elements
 from [l1] while possiblity changing the order. *)
@@ -287,7 +287,7 @@ Inductive submseteq {A} : relation (list A) :=
   | submseteq_cons x l1 l2 : submseteq l1 l2 → submseteq l1 (x :: l2)
   | submseteq_trans l1 l2 l3 : submseteq l1 l2 → submseteq l2 l3 → submseteq l1 l3.
 Infix "⊆+" := submseteq (at level 70) : stdpp_scope.
-Hint Extern 0 (_ ⊆+ _) => reflexivity.
+Hint Extern 0 (_ ⊆+ _) => reflexivity : core.
 
 (** Removes [x] from the list [l]. The function returns a [Some] when the
 +removal succeeds and [None] when [x] is not in [l]. *)
@@ -2760,7 +2760,7 @@ End Forall2_proper.
 
 Section Forall3.
   Context {A B C} (P : A → B → C → Prop).
-  Hint Extern 0 (Forall3 _ _ _ _) => constructor.
+  Hint Extern 0 (Forall3 _ _ _ _) => constructor : core.
 
   Lemma Forall3_app l1 l2 k1 k2 k1' k2' :
     Forall3 P l1 k1 k1' → Forall3 P l2 k2 k2' →
diff --git a/theories/numbers.v b/theories/numbers.v
index ef754a31a8829ed1c87c74c59dbef0a4da2cb83f..75c16661bcaa1cfe8fccd4c649ee286392d4dcd0 100644
--- a/theories/numbers.v
+++ b/theories/numbers.v
@@ -85,7 +85,7 @@ Instance: PartialOrder divide.
 Proof.
   repeat split; try apply _. intros ??. apply Nat.divide_antisym_nonneg; lia.
 Qed.
-Hint Extern 0 (_ | _) => reflexivity.
+Hint Extern 0 (_ | _) => reflexivity : core.
 Lemma Nat_divide_ne_0 x y : (x | y) → y ≠ 0 → x ≠ 0.
 Proof. intros Hxy Hy ->. by apply Hy, Nat.divide_0_l. Qed.
 
@@ -237,7 +237,7 @@ Instance N_le_po: PartialOrder (≤)%N.
 Proof.
   repeat split; red. apply N.le_refl. apply N.le_trans. apply N.le_antisymm.
 Qed.
-Hint Extern 0 (_ ≤ _)%N => reflexivity.
+Hint Extern 0 (_ ≤ _)%N => reflexivity : core.
 
 (** * Notations and properties of [Z] *)
 Open Scope Z_scope.
@@ -391,7 +391,7 @@ Notation "x ≤ y ≤ z ≤ z'" := (x ≤ y ∧ y ≤ z ∧ z ≤ z') : Qc_scope
 Notation "(≤)" := Qcle (only parsing) : Qc_scope.
 Notation "(<)" := Qclt (only parsing) : Qc_scope.
 
-Hint Extern 1 (_ ≤ _) => reflexivity || discriminate.
+Hint Extern 1 (_ ≤ _) => reflexivity || discriminate : core.
 Arguments Qred : simpl never.
 
 Instance Qc_eq_dec: EqDecision Qc := Qc_eq_dec.
@@ -537,7 +537,7 @@ Close Scope Qc_scope.
 (** The theory of positive rationals is very incomplete. We merely provide
 some operations and theorems that are relevant for fractional permissions. *)
 Record Qp := mk_Qp { Qp_car :> Qc ; Qp_prf : (0 < Qp_car)%Qc }.
-Hint Resolve Qp_prf.
+Hint Resolve Qp_prf : core.
 Delimit Scope Qp_scope with Qp.
 Bind Scope Qp_scope with Qp.
 Arguments Qp_car _%Qp : assert.
diff --git a/theories/option.v b/theories/option.v
index d9a554d9e8ad97e5041d8d7885f662efdad8a97c..db66b1a5207b0b8d175cc0b335a2571800c2949f 100644
--- a/theories/option.v
+++ b/theories/option.v
@@ -48,10 +48,10 @@ Proof. unfold is_Some. destruct mx; naive_solver. Qed.
 
 Lemma mk_is_Some {A} (mx : option A) x : mx = Some x → is_Some mx.
 Proof. intros; red; subst; eauto. Qed.
-Hint Resolve mk_is_Some.
+Hint Resolve mk_is_Some : core.
 Lemma is_Some_None {A} : ¬is_Some (@None A).
 Proof. by destruct 1. Qed.
-Hint Resolve is_Some_None.
+Hint Resolve is_Some_None : core.
 
 Lemma eq_None_not_Some {A} (mx : option A) : mx = None ↔ ¬is_Some mx.
 Proof. rewrite is_Some_alt; destruct mx; naive_solver. Qed.
diff --git a/theories/pmap.v b/theories/pmap.v
index 519641c22a88393dcdd9fd20642c05b68dc184d1..1a35e6d1fcda713514512890c9199c8de28a642f 100644
--- a/theories/pmap.v
+++ b/theories/pmap.v
@@ -13,8 +13,8 @@ From stdpp Require Export fin_maps.
 Set Default Proof Using "Type".
 
 Local Open Scope positive_scope.
-Local Hint Extern 0 (_ =@{positive} _) => congruence.
-Local Hint Extern 0 (_ ≠@{positive} _) => congruence.
+Local Hint Extern 0 (_ =@{positive} _) => congruence : core.
+Local Hint Extern 0 (_ ≠@{positive} _) => congruence : core.
 
 (** * The tree data structure *)
 (** The data type [Pmap_raw] specifies radix-2 search trees. These trees do
@@ -41,14 +41,14 @@ Lemma Pmap_wf_l {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf l.
 Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
 Lemma Pmap_wf_r {A} o (l r : Pmap_raw A) : Pmap_wf (PNode o l r) → Pmap_wf r.
 Proof. destruct o, l, r; simpl; rewrite ?andb_True; tauto. Qed.
-Local Hint Immediate Pmap_wf_l Pmap_wf_r.
+Local Hint Immediate Pmap_wf_l Pmap_wf_r : core.
 Definition PNode' {A} (o : option A) (l r : Pmap_raw A) :=
   match l, o, r with PLeaf, None, PLeaf => PLeaf | _, _, _ => PNode o l r end.
 Arguments PNode' : simpl never.
 Lemma PNode_wf {A} o (l r : Pmap_raw A) :
   Pmap_wf l → Pmap_wf r → Pmap_wf (PNode' o l r).
 Proof. destruct o, l, r; simpl; auto. Qed.
-Local Hint Resolve PNode_wf.
+Local Hint Resolve PNode_wf : core.
 
 (** Operations *)
 Instance Pempty_raw {A} : Empty (Pmap_raw A) := PLeaf.
diff --git a/theories/relations.v b/theories/relations.v
index 7b4370e16a9f1ea75052d02e02c1e9b193846f06..3d761f54387cd39206672af22053b5f97e711056 100644
--- a/theories/relations.v
+++ b/theories/relations.v
@@ -57,13 +57,13 @@ End definitions.
 (* Strongly normalizing elements *)
 Notation sn R := (Acc (flip R)).
 
-Hint Unfold nf red.
+Hint Unfold nf red : core.
 
 (** * General theorems *)
 Section rtc.
   Context `{R : relation A}.
 
-  Hint Constructors rtc nsteps bsteps tc.
+  Hint Constructors rtc nsteps bsteps tc : core.
 
   (* We give this instance a lower-than-usual priority because [setoid_rewrite]
      queries for [@Reflexive Prop ?r] in the hope of [iff_reflexive] getting
diff --git a/theories/set.v b/theories/set.v
index 39e389aed41a86f59a3a845d08440e3cd895736b..235900ea4257df136f60f4e2feec5bab5f6bf1b1 100644
--- a/theories/set.v
+++ b/theories/set.v
@@ -32,7 +32,7 @@ Lemma not_elem_of_mkSet {A} (P : A → Prop) x : x ∉ {[ x | P x ]} ↔ ¬P x.
 Proof. done. Qed.
 Lemma top_subseteq {A} (X : set A) : X ⊆ ⊤.
 Proof. done. Qed.
-Hint Resolve top_subseteq.
+Hint Resolve top_subseteq : core.
 
 Instance set_ret : MRet set := λ A (x : A), {[ x ]}.
 Instance set_bind : MBind set := λ A B (f : A → set B) (X : set A),