Merge pull request #252 from anton-trunov/implicit-core-hint-db

Fix some new warnings emitted by Coq 8.10

34 files changed, 105 insertions, 104 deletions

diff --git a/mathcomp/algebra/fraction.v b/mathcomp/algebra/fraction.v
index 28dd82b..dd3ce30 100644
--- a/mathcomp/algebra/fraction.v
+++ b/mathcomp/algebra/fraction.v
@@ -305,7 +305,7 @@ End FracField.
 
 Notation "{ 'fraction' T }" := (FracField.type_of (Phant T)).
 Notation equivf := (@FracField.equivf _).
-Hint Resolve denom_ratioP.
+Hint Resolve denom_ratioP : core.
 
 Section Canonicals.
 
diff --git a/mathcomp/algebra/intdiv.v b/mathcomp/algebra/intdiv.v
index 933bfcb..2f5e844 100644
--- a/mathcomp/algebra/intdiv.v
+++ b/mathcomp/algebra/intdiv.v
@@ -326,7 +326,7 @@ Proof. by rewrite !dvdzE abszM; apply: dvdn_mull. Qed.
 
 Lemma dvdz_mulr d m n : (d %| m)%Z -> (d %| m * n)%Z.
 Proof. by move=> d_m; rewrite mulrC dvdz_mull. Qed.
-Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr.
+Hint Resolve dvdz0 dvd1z dvdzz dvdz_mull dvdz_mulr : core.
 
 Lemma dvdz_mul d1 d2 m1 m2 : (d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2)%Z.
 Proof. by rewrite !dvdzE !abszM; apply: dvdn_mul. Qed.
diff --git a/mathcomp/algebra/interval.v b/mathcomp/algebra/interval.v
index 1ca3414..b5d58cb 100644
--- a/mathcomp/algebra/interval.v
+++ b/mathcomp/algebra/interval.v
@@ -187,12 +187,12 @@ Proof. by move: bl br => [[] a|] [[] b|]. Qed.
 Lemma le_boundr_refl : reflexive le_boundr.
 Proof. by move=> [[] b|]; rewrite /le_boundr /= ?lerr. Qed.
 
-Hint Resolve le_boundr_refl.
+Hint Resolve le_boundr_refl : core.
 
 Lemma le_boundl_refl : reflexive le_boundl.
 Proof. by move=> [[] b|]; rewrite /le_boundl /= ?lerr. Qed.
 
-Hint Resolve le_boundl_refl.
+Hint Resolve le_boundl_refl : core.
 
 Lemma le_boundl_bb x b1 b2 :
   le_boundl (BOpen_if b1 x) (BOpen_if b2 x) = (b1 ==> b2).
@@ -242,7 +242,7 @@ move=> x [[[] a|] [[] b|]]; move/itv_dec=> //= [hl hu]; do ?[split=> //;
     | by apply: negbTE; rewrite ltr_geF // (@ler_lt_trans _ x)].
 Qed.
 
-Hint Rewrite intP.
+Hint Rewrite intP : core.
 Arguments itvP [x i].
 
 Definition subitv (i1 i2 : interval R) :=
diff --git a/mathcomp/algebra/mxalgebra.v b/mathcomp/algebra/mxalgebra.v
index a8a91d3..7875b83 100644
--- a/mathcomp/algebra/mxalgebra.v
+++ b/mathcomp/algebra/mxalgebra.v
@@ -388,7 +388,7 @@ case: GaussE (IHm _ B) => [[L U] r] /= uL.
 rewrite unitmxE xrowE det_mulmx (@det_lblock _ 1) det1 mul1r unitrM.
 by rewrite -unitmxE unitmx_perm.
 Qed.
-Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit.
+Hint Resolve rank_leq_row rank_leq_col row_ebase_unit col_ebase_unit : core.
 
 Lemma mulmx_ebase m n (A : 'M_(m, n)) :
   col_ebase A *m pid_mx (\rank A) *m row_ebase A = A.
@@ -504,7 +504,7 @@ Arguments submxP {m1 m2 n A B}.
 
 Lemma submx_refl m n (A : 'M_(m, n)) : (A <= A)%MS.
 Proof. by rewrite submxE mulmx_coker. Qed.
-Hint Resolve submx_refl.
+Hint Resolve submx_refl : core.
 
 Lemma submxMl m n p (D : 'M_(m, n)) (A : 'M_(n, p)) : (D *m A <= A)%MS.
 Proof. by rewrite submxE -mulmxA mulmx_coker mulmx0. Qed.
@@ -874,7 +874,7 @@ Proof.
 apply/row_fullP; exists (pid_mx (\rank A) *m invmx (col_ebase A)).
 by rewrite !mulmxA mulmxKV // pid_mx_id // pid_mx_1.
 Qed.
-Hint Resolve row_base_free col_base_full.
+Hint Resolve row_base_free col_base_full : core.
 
 Lemma mxrank_leqif_sup m1 m2 n (A : 'M_(m1, n)) (B : 'M_(m2, n)) :
   (A <= B)%MS -> \rank A <= \rank B ?= iff (B <= A)%MS.
@@ -1974,7 +1974,7 @@ End Eigenspace.
 
 End RowSpaceTheory.
 
-Hint Resolve submx_refl.
+Hint Resolve submx_refl : core.
 Arguments submxP {F m1 m2 n A B}.
 Arguments eq_row_sub [F m n v A].
 Arguments row_subP {F m1 m2 n A B}.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index fe5de6d..f679828 100644
--- a/mathcomp/algebra/mxpoly.v
+++ b/mathcomp/algebra/mxpoly.v
@@ -899,7 +899,7 @@ apply: integral_horner_root mon_p pu0 intRp _.
 by apply/integral_poly => i; rewrite coefX; apply: integral_nat.
 Qed.
 
-Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K).
+Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core.
 
 Let XsubC0 (u : K) : root ('X - u%:P) u. Proof. by rewrite root_XsubC. Qed.
 Let intR_XsubC u :
diff --git a/mathcomp/algebra/polydiv.v b/mathcomp/algebra/polydiv.v
index 34b6e7b..026af3d 100644
--- a/mathcomp/algebra/polydiv.v
+++ b/mathcomp/algebra/polydiv.v
@@ -868,7 +868,7 @@ case: (eqVneq q 0) => [->|nzq]; last by rewrite expf_neq0 ?lead_coef_eq0.
 by rewrite /scalp 2!unlock /= eqxx lead_coef0 unitr0 /= oner_neq0.
 Qed.
 
-Hint Resolve lc_expn_scalp_neq0.
+Hint Resolve lc_expn_scalp_neq0 : core.
 
 Variant edivp_spec (m d : {poly R}) :
                                      nat * {poly R} * {poly R} -> bool -> Type :=
@@ -988,7 +988,7 @@ Qed.
 
 End WeakTheoryForIDomainPseudoDivision.
 
-Hint Resolve lc_expn_scalp_neq0.
+Hint Resolve lc_expn_scalp_neq0 : core.
 
 End WeakIdomain.
 
@@ -1049,7 +1049,7 @@ Proof.
 by rewrite /modp unlock redivp_def /=; case: ifP; rewrite rmodp1 // scaler0.
 Qed.
 
-Hint Resolve divp0 divp1 mod0p modp0 modp1.
+Hint Resolve divp0 divp1 mod0p modp0 modp1 : core.
 
 Lemma modp_small p q : size p < size q -> p %% q = p.
 Proof.
@@ -1156,7 +1156,7 @@ Qed.
 Lemma dvdp0 d : d %| 0.
 Proof. by rewrite /dvdp mod0p. Qed.
 
-Hint Resolve dvdp0.
+Hint Resolve dvdp0 : core.
 
 Lemma dvd0p p : (0 %| p) = (p == 0).
 Proof. by rewrite /dvdp modp0. Qed.
@@ -1231,7 +1231,7 @@ Qed.
 Lemma dvdpp d : d %| d.
 Proof. by rewrite /dvdp modpp. Qed.
 
-Hint Resolve dvdpp.
+Hint Resolve dvdpp : core.
 
 Lemma divp_dvd p q : (p %| q) -> ((q %/ p) %| q).
 Proof.
@@ -1253,7 +1253,7 @@ Qed.
 Lemma dvdp_mulr n d m : d %| m -> d %| m * n.
 Proof. by move=> hdm; rewrite mulrC dvdp_mull. Qed.
 
-Hint Resolve dvdp_mull dvdp_mulr.
+Hint Resolve dvdp_mull dvdp_mulr : core.
 
 Lemma dvdp_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
 Proof.
@@ -1468,7 +1468,7 @@ Qed.
 Lemma eqpxx : reflexive (@eqp R).
 Proof. by move=> p; rewrite /eqp dvdpp. Qed.
 
-Hint Resolve eqpxx.
+Hint Resolve eqpxx : core.
 
 Lemma eqp_sym : symmetric (@eqp R).
 Proof. by move=> p q; rewrite /eqp andbC. Qed.
@@ -2533,8 +2533,8 @@ Qed.
 
 End IDomainPseudoDivision.
 
-Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp.
-Hint Resolve dvdp0.
+Hint Resolve eqpxx divp0 divp1 mod0p modp0 modp1 dvdp_mull dvdp_mulr dvdpp : core.
+Hint Resolve dvdp0 : core.
 
 End CommonIdomain.
 
diff --git a/mathcomp/algebra/rat.v b/mathcomp/algebra/rat.v
index 6015f33..14fde5a 100644
--- a/mathcomp/algebra/rat.v
+++ b/mathcomp/algebra/rat.v
@@ -56,7 +56,7 @@ Definition denq x := nosimpl ((valq x).2).
 
 Lemma denq_gt0  x : 0 < denq x.
 Proof. by rewrite /denq; case: x=> [[a b] /= /andP []]. Qed.
-Hint Resolve denq_gt0.
+Hint Resolve denq_gt0 : core.
 
 Definition denq_ge0 x := ltrW (denq_gt0 x).
 
@@ -64,7 +64,7 @@ Lemma denq_lt0  x : (denq x < 0) = false. Proof. by rewrite ltr_gtF. Qed.
 
 Lemma denq_neq0 x : denq x != 0.
 Proof. by rewrite /denq gtr_eqF ?denq_gt0. Qed.
-Hint Resolve denq_neq0.
+Hint Resolve denq_neq0 : core.
 
 Lemma denq_eq0 x : (denq x == 0) = false.
 Proof. exact: negPf (denq_neq0 _). Qed.
@@ -368,7 +368,7 @@ Qed.
 Notation "n %:Q" := ((n : int)%:~R : rat)
   (at level 2, left associativity, format "n %:Q")  : ring_scope.
 
-Hint Resolve denq_neq0 denq_gt0 denq_ge0.
+Hint Resolve denq_neq0 denq_gt0 denq_ge0 : core.
 
 Definition subq (x y : rat) : rat := (addq x (oppq y)).
 Definition divq (x y : rat) : rat := (mulq x (invq y)).
diff --git a/mathcomp/algebra/ssralg.v b/mathcomp/algebra/ssralg.v
index 5542959..40a1f83 100644
--- a/mathcomp/algebra/ssralg.v
+++ b/mathcomp/algebra/ssralg.v
@@ -1305,7 +1305,7 @@ Hypothesis charFp : p \in [char R].
 
 Lemma charf0 : p%:R = 0 :> R. Proof. by apply/eqP; case/andP: charFp. Qed.
 Lemma charf_prime : prime p. Proof. by case/andP: charFp. Qed.
-Hint Resolve charf_prime.
+Hint Resolve charf_prime : core.
 
 Lemma mulrn_char x : x *+ p = 0. Proof. by rewrite -mulr_natl charf0 mul0r. Qed.
 
diff --git a/mathcomp/algebra/ssrint.v b/mathcomp/algebra/ssrint.v
index 614fbc2..b734ad7 100644
--- a/mathcomp/algebra/ssrint.v
+++ b/mathcomp/algebra/ssrint.v
@@ -967,7 +967,7 @@ Proof. by rewrite mulrz_eq0 negb_or. Qed.
 
 Lemma realz n : (n%:~R : R) \in Num.real.
 Proof. by rewrite -topredE /Num.real /= ler0z lerz0 ler_total. Qed.
-Hint Resolve realz.
+Hint Resolve realz : core.
 
 Definition intr_inj := @mulrIz 1 (oner_neq0 R).
 
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v
index ae0c00b..2414e13 100644
--- a/mathcomp/algebra/ssrnum.v
+++ b/mathcomp/algebra/ssrnum.v
@@ -1045,7 +1045,7 @@ Lemma realE x : (x \is real) = (0 <= x) || (x <= 0). Proof. by []. Qed.
 Lemma lerr x : x <= x. Proof. exact: lerr. Qed.
 Lemma ltrr x : x < x = false. Proof. by rewrite ltr_def eqxx. Qed.
 Lemma ltrW x y : x < y -> x <= y. Proof. exact: ltrW. Qed.
-Hint Resolve lerr ltrr ltrW.
+Hint Resolve lerr ltrr ltrW : core.
 
 Lemma ltr_neqAle x y : (x < y) = (x != y) && (x <= y).
 Proof. by rewrite ltr_def eq_sym. Qed.
@@ -1080,12 +1080,12 @@ Qed.
 Lemma ler01 : 0 <= 1 :> R. Proof. exact: ler01. Qed.
 Lemma ltr01 : 0 < 1 :> R. Proof. exact: ltr01. Qed.
 Lemma ler0n n : 0 <= n%:R :> R. Proof. by rewrite -nnegrE rpred_nat. Qed.
-Hint Resolve ler01 ltr01 ler0n.
+Hint Resolve ler01 ltr01 ler0n : core.
 Lemma ltr0Sn n : 0 < n.+1%:R :> R.
 Proof. by elim: n => // n; apply: addr_gt0. Qed.
 Lemma ltr0n n : (0 < n%:R :> R) = (0 < n)%N.
 Proof. by case: n => //= n; apply: ltr0Sn. Qed.
-Hint Resolve ltr0Sn.
+Hint Resolve ltr0Sn : core.
 
 Lemma pnatr_eq0 n : (n%:R == 0 :> R) = (n == 0)%N.
 Proof. by case: n => [|n]; rewrite ?mulr0n ?eqxx // gtr_eqF. Qed.
@@ -1154,7 +1154,7 @@ by rewrite -{2}normrN -normr0 -(subrr x) ler_norm_add.
 Qed.
 
 Lemma normr_ge0 x : 0 <= `|x|. Proof. by rewrite ger0_def normr_id. Qed.
-Hint Resolve normr_ge0.
+Hint Resolve normr_ge0 : core.
 
 Lemma ler0_norm x : x <= 0 -> `|x| = - x.
 Proof. by move=> x_le0; rewrite -[r in _ = r]ger0_norm ?normrN ?oppr_ge0. Qed.
@@ -1263,7 +1263,7 @@ Arguments ltr01 {R}.
 Arguments normr_idP {R x}.
 Arguments normr0P {R x}.
 Arguments lerifP {R x y C}.
-Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0.
+Hint Resolve @ler01 @ltr01 lerr ltrr ltrW ltr_eqF ltr0Sn ler0n normr_ge0 : core.
 
 Section NumIntegralDomainMonotonyTheory.
 
@@ -1450,10 +1450,10 @@ Implicit Types x y z t : R.
 
 Lemma ler_opp2 : {mono -%R : x y /~ x <= y :> R}.
 Proof. by move=> x y /=; rewrite -subr_ge0 opprK addrC subr_ge0. Qed.
-Hint Resolve ler_opp2.
+Hint Resolve ler_opp2 : core.
 Lemma ltr_opp2 : {mono -%R : x y /~ x < y :> R}.
 Proof. by move=> x y /=; rewrite lerW_nmono. Qed.
-Hint Resolve ltr_opp2.
+Hint Resolve ltr_opp2 : core.
 Definition lter_opp2 := (ler_opp2, ltr_opp2).
 
 Lemma ler_oppr x y : (x <= - y) = (y <= - x).
@@ -1525,10 +1525,10 @@ Lemma ltr0_real x : x < 0 -> x \is real.
 Proof. by move=> /ltrW/ler0_real. Qed.
 
 Lemma real0 : 0 \is @real R. Proof. by rewrite ger0_real. Qed.
-Hint Resolve real0.
+Hint Resolve real0 : core.
 
 Lemma real1 : 1 \is @real R. Proof. by rewrite ger0_real. Qed.
-Hint Resolve real1.
+Hint Resolve real1 : core.
 
 Lemma realn n : n%:R \is @real R. Proof. by rewrite ger0_real. Qed.
 
@@ -2640,7 +2640,7 @@ Qed.
 (* norm + add *)
 
 Lemma normr_real x : `|x| \is real. Proof. by rewrite ger0_real. Qed.
-Hint Resolve normr_real.
+Hint Resolve normr_real : core.
 
 Lemma ler_norm_sum I r (G : I -> R) (P : pred I):
   `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i|.
@@ -3144,7 +3144,7 @@ Qed.
 
 End NumDomainOperationTheory.
 
-Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real.
+Hint Resolve ler_opp2 ltr_opp2 real0 real1 normr_real : core.
 Arguments ler_sqr {R} [x y].
 Arguments ltr_sqr {R} [x y].
 Arguments signr_inj {R} [x1 x2].
@@ -3429,13 +3429,13 @@ End NumFieldTheory.
 
 Section RealDomainTheory.
 
-Hint Resolve lerr.
+Hint Resolve lerr : core.
 
 Variable R : realDomainType.
 Implicit Types x y z t : R.
 
 Lemma num_real x : x \is real. Proof. exact: num_real. Qed.
-Hint Resolve num_real.
+Hint Resolve num_real : core.
 
 Lemma ler_total : total (@le R). Proof. by move=> x y; apply: real_leVge. Qed.
 
@@ -3534,14 +3534,14 @@ Proof. by rewrite -real_normrEsign. Qed.
 
 End RealDomainTheory.
 
-Hint Resolve num_real.
+Hint Resolve num_real : core.
 
 Section RealDomainMonotony.
 
 Variables (R : realDomainType) (R' : numDomainType) (D : pred R) (f : R -> R').
 Implicit Types (m n p : nat) (x y z : R) (u v w : R').
 
-Hint Resolve (@num_real R).
+Hint Resolve (@num_real R) : core.
 
 Lemma homo_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y}.
 Proof. by move=> mf x y; apply: real_mono. Qed.
@@ -3569,7 +3569,7 @@ Section RealDomainOperations.
 
 Variable R : realDomainType.
 Implicit Types x y z t : R.
-Hint Resolve (@num_real R).
+Hint Resolve (@num_real R) : core.
 
 Lemma sgr_cp0 x :
   ((sg x == 1) = (0 < x)) *
@@ -4032,7 +4032,7 @@ Lemma poly_ivt : real_closed_axiom R. Proof. exact: poly_ivt. Qed.
 
 Lemma sqrtr_ge0 a : 0 <= sqrt a.
 Proof. by rewrite /sqrt; case: (sig2W _). Qed.
-Hint Resolve sqrtr_ge0.
+Hint Resolve sqrtr_ge0 : core.
 
 Lemma sqr_sqrtr a : 0 <= a -> sqrt a ^+ 2 = a.
 Proof.
@@ -4325,7 +4325,7 @@ Proof.
 rewrite CrealE fmorph_div rmorph_nat rmorphM rmorphB conjCK.
 by rewrite conjCi -opprB mulrNN.
 Qed.
-Hint Resolve Creal_Re Creal_Im.
+Hint Resolve Creal_Re Creal_Im : core.
 
 Fact Re_is_additive : additive Re.
 Proof. by move=> x y; rewrite /Re rmorphB addrACA -opprD mulrBl. Qed.
diff --git a/mathcomp/algebra/vector.v b/mathcomp/algebra/vector.v
index 75b2073..c4c62c3 100644
--- a/mathcomp/algebra/vector.v
+++ b/mathcomp/algebra/vector.v
@@ -460,7 +460,7 @@ by have:= sU12 (r2v u); rewrite !memvE /subsetv !genmxE r2vK.
 Qed.
 
 Lemma subvv U : (U <= U)%VS. Proof. exact/subvP. Qed.
-Hint Resolve subvv.
+Hint Resolve subvv : core.
 
 Lemma subv_trans : transitive subV.
 Proof. by move=> U V W /subvP sUV /subvP sVW; apply/subvP=> u /sUV/sVW. Qed.
@@ -1222,7 +1222,7 @@ End BigSumBasis.
 
 End VectorTheory.
 
-Hint Resolve subvv.
+Hint Resolve subvv : core.
 Arguments subvP {K vT U V}.
 Arguments addv_idPl {K vT U V}.
 Arguments addv_idPr {K vT U V}.
diff --git a/mathcomp/character/character.v b/mathcomp/character/character.v
index a657fa5..9a61ebe 100644
--- a/mathcomp/character/character.v
+++ b/mathcomp/character/character.v
@@ -576,7 +576,7 @@ Proof. by move=> i; rewrite /irr_of_socle enum_valK cast_ordK addrK. Qed.
 
 Lemma irr_of_socleK : cancel irr_of_socle W.
 Proof. by move=> Wi; rewrite /W subrK cast_ordKV enum_rankK. Qed.
-Hint Resolve socle_of_IirrK irr_of_socleK.
+Hint Resolve socle_of_IirrK irr_of_socleK : core.
 
 Lemma irr_of_socle_bij (A : pred (Iirr G)) : {on A, bijective irr_of_socle}.
 Proof. by apply: onW_bij; exists W. Qed.
diff --git a/mathcomp/character/classfun.v b/mathcomp/character/classfun.v
index 7b2b90d..a4ecd2c 100644
--- a/mathcomp/character/classfun.v
+++ b/mathcomp/character/classfun.v
@@ -759,7 +759,7 @@ Arguments classfun_on {gT} B%g A%g.
 Notation "''CF' ( G , A )" := (classfun_on G A) : ring_scope.
 
 Arguments cfun_onP {gT G A phi}.
-Hint Resolve cfun_onT.
+Hint Resolve cfun_onT : core.
 
 Section DotProduct.
 
diff --git a/mathcomp/character/mxabelem.v b/mathcomp/character/mxabelem.v
index 69055d4..22ab389 100644
--- a/mathcomp/character/mxabelem.v
+++ b/mathcomp/character/mxabelem.v
@@ -511,7 +511,7 @@ Proof. by rewrite im_abelem_rV inE. Qed.
 
 Lemma sub_im_abelem_rV mA : subset mA (mem (ErV @* E)).
 Proof. by rewrite unlock; apply/pred0P=> v /=; rewrite mem_im_abelem_rV. Qed.
-Hint Resolve mem_im_abelem_rV sub_im_abelem_rV.
+Hint Resolve mem_im_abelem_rV sub_im_abelem_rV : core.
 
 Lemma abelem_rV_1 : ErV 1 = 0%R. Proof. by rewrite morph1. Qed.
 
@@ -552,7 +552,7 @@ Proof. by rewrite -im_rVabelem mem_morphim. Qed.
 
 Lemma sub_rVabelem L : rV_E @* L \subset E.
 Proof. by rewrite -[_ @* L]morphimIim im_invm subsetIl. Qed.
-Hint Resolve mem_rVabelem sub_rVabelem.
+Hint Resolve mem_rVabelem sub_rVabelem : core.
 
 Lemma card_rVabelem L : #|rV_E @* L| = #|L|.
 Proof. by rewrite card_injm ?rVabelem_injm. Qed.
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v
index 4b37a9c..fc01763 100644
--- a/mathcomp/field/algC.v
+++ b/mathcomp/field/algC.v
@@ -607,7 +607,7 @@ Local Notation intrp := (map_poly intr).
 Local Notation pZtoQ := (map_poly ZtoQ).
 Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
-Local Hint Resolve (@intr_inj _ : injective ZtoC).
+Local Hint Resolve (@intr_inj _ : injective ZtoC) : core.
 
 (* Specialization of a few basic ssrnum order lemmas. *)
 
@@ -645,7 +645,8 @@ Definition algC_algebraic x := Algebraics.Implementation.algebraic x.
 
 Lemma Creal0 : 0 \is Creal. Proof. exact: rpred0. Qed.
 Lemma Creal1 : 1 \is Creal. Proof. exact: rpred1. Qed.
-Hint Resolve Creal0 Creal1. (* Trivial cannot resolve a general real0 hint. *)
+(* Trivial cannot resolve a general real0 hint. *)
+Hint Resolve Creal0 Creal1 : core. 
 
 Lemma algCrect x : x = 'Re x + 'i * 'Im x.
 Proof. by rewrite [LHS]Crect. Qed.
@@ -655,7 +656,7 @@ Proof. by rewrite Creal_Re. Qed.
 
 Lemma algCreal_Im x : 'Im x \is Creal.
 Proof. by rewrite Creal_Im. Qed.
-Hint Resolve algCreal_Re algCreal_Im.
+Hint Resolve algCreal_Re algCreal_Im : core.
 
 (* Integer subset. *)
 (* Not relying on the undocumented interval library, for now. *)
@@ -680,7 +681,7 @@ Lemma floorCK : {in Cint, cancel floorC intr}. Proof. by move=> z /eqP. Qed.
 
 Lemma floorC0 : floorC 0 = 0. Proof. exact: (intCK 0). Qed.
 Lemma floorC1 : floorC 1 = 1. Proof. exact: (intCK 1). Qed.
-Hint Resolve floorC0 floorC1.
+Hint Resolve floorC0 floorC1 : core.
 
 Lemma floorCpK (p : {poly algC}) :
   p \is a polyOver Cint -> map_poly intr (map_poly floorC p) = p.
@@ -723,7 +724,7 @@ Proof. by case/CintP=> m ->; apply: rpred_int. Qed.
 
 Lemma Cint0 : 0 \in Cint. Proof. exact: (Cint_int 0). Qed.
 Lemma Cint1 : 1 \in Cint. Proof. exact: (Cint_int 1). Qed.
-Hint Resolve Cint0 Cint1.
+Hint Resolve Cint0 Cint1 : core.
 
 Fact Cint_key : pred_key Cint. Proof. by []. Qed.
 Fact Cint_subring : subring_closed Cint.
@@ -814,7 +815,7 @@ Proof. by case/CnatP=> n ->; apply: rpred_nat. Qed.
 Lemma Cnat_nat n : n%:R \in Cnat. Proof. by apply/CnatP; exists n. Qed.
 Lemma Cnat0 : 0 \in Cnat. Proof. exact: (Cnat_nat 0). Qed.
 Lemma Cnat1 : 1 \in Cnat. Proof. exact: (Cnat_nat 1). Qed.
-Hint Resolve Cnat_nat Cnat0 Cnat1.
+Hint Resolve Cnat_nat Cnat0 Cnat1 : core.
 
 Fact Cnat_key : pred_key Cnat. Proof. by []. Qed.
 Fact Cnat_semiring : semiring_closed Cnat.
@@ -970,7 +971,7 @@ Proof. by move=> x_dv_y /dvdCP[m Zm ->]; apply: dvdC_mull. Qed.
 
 Lemma dvdC_refl x : (x %| x)%C.
 Proof. by apply/dvdCP; exists 1; rewrite ?mul1r. Qed.
-Hint Resolve dvdC_refl.
+Hint Resolve dvdC_refl : core.
 
 Fact dvdC_key x : pred_key (dvdC x). Proof. by []. Qed.
 Lemma dvdC_zmod x : zmod_closed (dvdC x).
@@ -1004,7 +1005,7 @@ Lemma eqCmod_refl e x : (x == x %[mod e])%C.
 Proof. by rewrite /eqCmod subrr rpred0. Qed.
 
 Lemma eqCmodm0 e : (e == 0 %[mod e])%C. Proof. by rewrite /eqCmod subr0. Qed.
-Hint Resolve eqCmod_refl eqCmodm0.
+Hint Resolve eqCmod_refl eqCmodm0 : core.
 
 Lemma eqCmod0 e x : (x == 0 %[mod e])%C = (e %| x)%C.
 Proof. by rewrite /eqCmod subr0. Qed.
@@ -1091,7 +1092,7 @@ Qed.
 
 Lemma Crat0 : 0 \in Crat. Proof. by apply/CratP; exists 0; rewrite rmorph0. Qed.
 Lemma Crat1 : 1 \in Crat. Proof. by apply/CratP; exists 1; rewrite rmorph1. Qed.
-Hint Resolve Crat0 Crat1.
+Hint Resolve Crat0 Crat1 : core.
 
 Fact Crat_key : pred_key Crat. Proof. by []. Qed.
 Fact Crat_divring_closed : divring_closed Crat.
@@ -1236,5 +1237,5 @@ Proof. by move=> _ u /CintP[m ->]; apply: rpredZint. Qed.
 End PredCmod.
 
 End AlgebraicsTheory.
-Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1.
-Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0.
+Hint Resolve Creal0 Creal1 Cnat_nat Cnat0 Cnat1 Cint0 Cint1 floorC0 Crat0 Crat1 : core.
+Hint Resolve dvdC0 dvdC_refl eqCmod_refl eqCmodm0 : core.
diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
index 5d78cac..1db4aa4 100644
--- a/mathcomp/field/algnum.v
+++ b/mathcomp/field/algnum.v
@@ -56,7 +56,7 @@ Local Notation pZtoQ := (map_poly ZtoQ).
 Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
 
-Local Hint Resolve (@intr_inj _ : injective ZtoC).
+Local Hint Resolve (@intr_inj _ : injective ZtoC) : core.
 Local Notation QtoCm := [rmorphism of QtoC].
 
 (* Number fields and rational spans. *)
@@ -550,7 +550,7 @@ Proof. by rewrite Aint_Cint ?Cint_int. Qed.
 
 Lemma Aint0 : 0 \in Aint. Proof. exact: (Aint_int 0). Qed.
 Lemma Aint1 : 1 \in Aint. Proof. exact: (Aint_int 1). Qed.
-Hint Resolve Aint0 Aint1.
+Hint Resolve Aint0 Aint1 : core.
 
 Lemma Aint_unity_root n x : (n > 0)%N -> n.-unity_root x -> x \in Aint.
 Proof.
@@ -702,7 +702,7 @@ Notation "x != y %[mod e ]" := (~~ (eqAmod e x y)) : algC_scope.
 
 Lemma eqAmod_refl e x : (x == x %[mod e])%A.
 Proof. by rewrite /eqAmod subrr rpred0. Qed.
-Hint Resolve eqAmod_refl.
+Hint Resolve eqAmod_refl : core.
 
 Lemma eqAmod_sym e x y : ((x == y %[mod e]) = (y == x %[mod e]))%A.
 Proof. by rewrite /eqAmod -opprB rpredN. Qed.
@@ -739,7 +739,7 @@ Qed.
 
 Lemma eqAmodm0 e : (e == 0 %[mod e])%A.
 Proof. by rewrite /eqAmod subr0 unfold_in; case: ifPn => // /divff->. Qed.
-Hint Resolve eqAmodm0.
+Hint Resolve eqAmodm0 : core.
 
 Lemma eqAmodMr e :
   {in Aint, forall z x y, x == y %[mod e] -> x * z == y * z %[mod e]}%A.
diff --git a/mathcomp/field/closed_field.v b/mathcomp/field/closed_field.v
index 009c1ae..76039d1 100644
--- a/mathcomp/field/closed_field.v
+++ b/mathcomp/field/closed_field.v
@@ -95,7 +95,7 @@ Definition qf_cps T D (x : cps T) :=
 
 Lemma qf_cps_ret T D (x : T) : D x -> qf_cps D (ret x).
 Proof. move=> ??; exact. Qed.
-Hint Resolve qf_cps_ret.
+Hint Resolve qf_cps_ret : core.
 
 Lemma qf_cps_bind T1 D1 T2 D2 (x : cps T1) (f : T1 -> cps T2) :
   qf_cps D1 x -> (forall x, D1 x -> qf_cps D2 (f x)) -> qf_cps D2 (bind x f).
diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index 80bdf50..afb0b0b 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -122,7 +122,7 @@ Local Notation pZtoQ := (map_poly ZtoQ).
 Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
 
-Local Hint Resolve (@intr_inj [numDomainType of algC]).
+Local Hint Resolve (@intr_inj [numDomainType of algC]) : core.
 Local Notation QtoC_M := (ratr_rmorphism [numFieldType of algC]).
 
 Lemma C_prim_root_exists n : (n > 0)%N -> {z : algC | n.-primitive_root z}.
diff --git a/mathcomp/fingroup/automorphism.v b/mathcomp/fingroup/automorphism.v
index 320331c..5f28b7d 100644
--- a/mathcomp/fingroup/automorphism.v
+++ b/mathcomp/fingroup/automorphism.v
@@ -449,7 +449,7 @@ End Characteristicity.
 
 Arguments characteristic _ _%g _%g.
 Notation "H \char G" := (characteristic H G) : group_scope.
-Hint Resolve char_refl.
+Hint Resolve char_refl : core.
 
 Section InjmChar.
 
diff --git a/mathcomp/fingroup/fingroup.v b/mathcomp/fingroup/fingroup.v
index 19cefcd..f436102 100644
--- a/mathcomp/fingroup/fingroup.v
+++ b/mathcomp/fingroup/fingroup.v
@@ -492,7 +492,7 @@ Qed.
 
 End PreGroupIdentities.
 
-Hint Resolve commute1.
+Hint Resolve commute1 : core.
 Arguments invg_inj {T} [x1 x2].
 Prenex Implicits commute invgK.
 
@@ -1358,7 +1358,7 @@ Lemma valG : val G = G. Proof. by []. Qed.
 (* Non-triviality. *)
 
 Lemma group1 : 1 \in G. Proof. by case/group_setP: (valP G). Qed.
-Hint Resolve group1.
+Hint Resolve group1 : core.
 
 (* Loads of silly variants to placate the incompleteness of trivial. *)
 (* An alternative would be to upgrade done, pending better support   *)
@@ -1647,7 +1647,7 @@ Proof. by move=> y Gy /=; rewrite -class_rcoset rcoset_id. Qed.
 
 Lemma class_refl x : x \in x ^: G.
 Proof. by apply/imsetP; exists 1; rewrite ?conjg1. Qed.
-Hint Resolve class_refl.
+Hint Resolve class_refl : core.
 
 Lemma class_eqP x y : reflect (x ^: G = y ^: G) (x \in y ^: G).
 Proof.
@@ -1794,7 +1794,7 @@ Proof. by move=> x y Gx Gy; apply: val_inj; rewrite /= !subgK ?groupM. Qed.
 
 End OneGroup.
 
-Hint Resolve group1.
+Hint Resolve group1 : core.
 
 Lemma groupD1_inj G H : G^# = H^# -> G :=: H.
 Proof. by move/(congr1 (setU 1)); rewrite !setD1K. Qed.
@@ -1842,9 +1842,9 @@ Qed.
 
 End GroupProp.
 
-Hint Resolve group1 group1_class1 group1_class12 group1_class12.
-Hint Resolve group1_eqType group1_finType.
-Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0.
+Hint Resolve group1 group1_class1 group1_class12 group1_class12 : core.
+Hint Resolve group1_eqType group1_finType : core.
+Hint Resolve cardG_gt0 cardG_gt0_reduced indexg_gt0 : core.
 
 Notation "G :^ x" := (conjG_group G x) : Group_scope.
 
@@ -1907,7 +1907,7 @@ Proof. exact: cardG_gt0. Qed.
 
 End GroupInter.
 
-Hint Resolve order_gt0.
+Hint Resolve order_gt0 : core.
 
 Arguments generated_group _ _%g.
 Arguments joing_group _ _%g _%g.
@@ -3005,7 +3005,7 @@ Notation "''C_' G [ x ]" := (setI_group G 'C[x]) : Group_scope.
 Notation "''C_' ( G ) [ x ]" := (setI_group G 'C[x])
   (only parsing) : Group_scope.
 
-Hint Resolve normG normal_refl.
+Hint Resolve normG normal_refl : core.
 
 Section MinMaxGroup.
 
diff --git a/mathcomp/fingroup/morphism.v b/mathcomp/fingroup/morphism.v
index 4b2d863..cb02991 100644
--- a/mathcomp/fingroup/morphism.v
+++ b/mathcomp/fingroup/morphism.v
@@ -1495,7 +1495,7 @@ Proof. by apply/injmP; apply: in2W; apply: subg_inj. Qed.
 
 Lemma injm_subg : 'injm (subg G).
 Proof. by apply/injmP; apply: can_in_inj (@subgK _ _). Qed.
-Hint Resolve injm_sgval injm_subg.
+Hint Resolve injm_sgval injm_subg : core.
 
 Lemma ker_sgval : 'ker sgval = 1. Proof. exact/trivgP. Qed.
 Lemma ker_subg : 'ker (subg G) = 1. Proof. exact/trivgP. Qed.
diff --git a/mathcomp/fingroup/perm.v b/mathcomp/fingroup/perm.v
index 01ef08e..b1a7dd7 100644
--- a/mathcomp/fingroup/perm.v
+++ b/mathcomp/fingroup/perm.v
@@ -129,7 +129,7 @@ Lemma perm_inj s : injective s.
 Proof. by rewrite -!pvalE; apply: (injectiveP _ (valP s)). Qed.
 
 Arguments perm_inj : clear implicits.
-Hint Resolve perm_inj.
+Hint Resolve perm_inj : core.
 
 Lemma perm_onto s : codom s =i predT.
 Proof. by apply/subset_cardP; rewrite ?card_codom ?subset_predT. Qed.
diff --git a/mathcomp/solvable/abelian.v b/mathcomp/solvable/abelian.v
index 746898f..16ce432 100644
--- a/mathcomp/solvable/abelian.v
+++ b/mathcomp/solvable/abelian.v
@@ -249,7 +249,7 @@ Proof. by apply/dvdn_biglcmP=> x Gx; apply: order_dvdG. Qed.
 
 Lemma exponent_gt0 G : 0 < exponent G.
 Proof. exact: dvdn_gt0 (exponent_dvdn G). Qed.
-Hint Resolve exponent_gt0.
+Hint Resolve exponent_gt0 : core.
 
 Lemma pnat_exponent pi G : pi.-nat (exponent G) = pi.-group G.
 Proof.
diff --git a/mathcomp/solvable/center.v b/mathcomp/solvable/center.v
index 88774db..e2c6f48 100644
--- a/mathcomp/solvable/center.v
+++ b/mathcomp/solvable/center.v
@@ -375,7 +375,7 @@ rewrite /cpairg1 /cpair1g; do 2!case: restrmP => _ [_ _ _ -> //].
 rewrite !morphim_comp morphim_cents // morphim_pair1g morphim_pairg1.
 by case/dprodP: (setX_dprod H K).
 Qed.
-Hint Resolve im_cpair_cent.
+Hint Resolve im_cpair_cent : core.
 
 Lemma im_cpair : CH * CK = C.
 Proof.
diff --git a/mathcomp/ssreflect/bigop.v b/mathcomp/ssreflect/bigop.v
index 2db8927..f108ff9 100644
--- a/mathcomp/ssreflect/bigop.v
+++ b/mathcomp/ssreflect/bigop.v
@@ -558,7 +558,7 @@ Qed.
 
 Lemma mem_index_enum T i : i \in index_enum T.
 Proof. by rewrite -[index_enum T]enumT mem_enum. Qed.
-Hint Resolve mem_index_enum.
+Hint Resolve mem_index_enum : core.
 
 Lemma filter_index_enum T P : filter P (index_enum T) = enum P.
 Proof. by []. Qed.
diff --git a/mathcomp/ssreflect/div.v b/mathcomp/ssreflect/div.v
index ed1eedf..80c9312 100644
--- a/mathcomp/ssreflect/div.v
+++ b/mathcomp/ssreflect/div.v
@@ -327,7 +327,7 @@ Proof. by case/dvdnP=> n' ->; rewrite /dvdn mulnA modnMl. Qed.
 
 Lemma dvdn_mulr d m n : d %| m -> d %| m * n.
 Proof. by move=> d_m; rewrite mulnC dvdn_mull. Qed.
-Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr.
+Hint Resolve dvdn0 dvd1n dvdnn dvdn_mull dvdn_mulr : core.
 
 Lemma dvdn_mul d1 d2 m1 m2 : d1 %| m1 -> d2 %| m2 -> d1 * d2 %| m1 * m2.
 Proof.
@@ -462,7 +462,7 @@ case: m => //= m; elim: n => //= n IHn; rewrite ltnS leq_eqVlt.
 by case/predU1P=> [-> | /IHn]; [apply: dvdn_mulr | apply: dvdn_mull].
 Qed.
 
-Hint Resolve dvdn_add dvdn_sub dvdn_exp.
+Hint Resolve dvdn_add dvdn_sub dvdn_exp : core.
 
 Lemma eqn_mod_dvd d m n : n <= m -> (m == n %[mod d]) = (d %| m - n).
 Proof.
diff --git a/mathcomp/ssreflect/eqtype.v b/mathcomp/ssreflect/eqtype.v
index 6ed4b97..dc3daf0 100644
--- a/mathcomp/ssreflect/eqtype.v
+++ b/mathcomp/ssreflect/eqtype.v
@@ -196,7 +196,7 @@ Notation eqxx := eq_refl.
 Lemma eq_sym (T : eqType) (x y : T) : (x == y) = (y == x).
 Proof. exact/eqP/eqP. Qed.
 
-Hint Resolve eq_refl eq_sym.
+Hint Resolve eq_refl eq_sym : core.
 
 Section Contrapositives.
 
diff --git a/mathcomp/ssreflect/fingraph.v b/mathcomp/ssreflect/fingraph.v
index c534b7b..5358dc7 100644
--- a/mathcomp/ssreflect/fingraph.v
+++ b/mathcomp/ssreflect/fingraph.v
@@ -216,7 +216,7 @@ Definition closure_mem m_a : pred T :=
 
 End Connect.
 
-Hint Resolve connect0.
+Hint Resolve connect0 : core.
 
 Notation n_comp e a := (n_comp_mem e (mem a)).
 Notation closed e a := (closed_mem e (mem a)).
diff --git a/mathcomp/ssreflect/finset.v b/mathcomp/ssreflect/finset.v
index 4ad02c6..9ca96c8 100644
--- a/mathcomp/ssreflect/finset.v
+++ b/mathcomp/ssreflect/finset.v
@@ -244,7 +244,7 @@ End BasicSetTheory.
 Definition inE := (in_set, inE).
 
 Arguments set0 {T}.
-Hint Resolve in_setT.
+Hint Resolve in_setT : core.
 
 Notation "[ 'set' : T ]" := (setTfor (Phant T))
   (at level 0, format "[ 'set' :  T ]") : set_scope.
@@ -348,7 +348,7 @@ Proof. by apply/subsetP=> x; rewrite inE. Qed.
 
 Lemma subsetT_hint mA : subset mA (mem [set: T]).
 Proof. by rewrite unlock; apply/pred0P=> x; rewrite !inE. Qed.
-Hint Resolve subsetT_hint.
+Hint Resolve subsetT_hint : core.
 
 Lemma subTset A : (setT \subset A) = (A == setT).
 Proof. by rewrite eqEsubset subsetT. Qed.
@@ -975,7 +975,7 @@ Arguments subUsetP {T A B C}.
 Arguments subsetDP {T A B C}.
 Arguments subsetD1P {T A B x}.
 Prenex Implicits set1.
-Hint Resolve subsetT_hint.
+Hint Resolve subsetT_hint : core.
 
 Section setOpsAlgebra.
 
diff --git a/mathcomp/ssreflect/fintype.v b/mathcomp/ssreflect/fintype.v
index 8be2eb0..441fc12 100644
--- a/mathcomp/ssreflect/fintype.v
+++ b/mathcomp/ssreflect/fintype.v
@@ -626,7 +626,7 @@ Lemma subxx_hint (mA : mem_pred T) : subset mA mA.
 Proof.
 by case: mA => A; have:= introT (subsetP A A); rewrite !unlock => ->.
 Qed.
-Hint Resolve subxx_hint.
+Hint Resolve subxx_hint : core.
 
 (* The parametrization by predType makes it easier to apply subxx. *)
 Lemma subxx (pT : predType T) (pA : pT) : pA \subset pA.
@@ -818,7 +818,7 @@ Proof. by rewrite !disjoint_has has_cat negb_or. Qed.
 
 End OpsTheory.
 
-Hint Resolve subxx_hint.
+Hint Resolve subxx_hint : core.
 
 Arguments pred0P {T P}.
 Arguments pred0Pn {T P}.
@@ -1585,7 +1585,7 @@ End OrdinalSub.
 Notation "''I_' n" := (ordinal n)
   (at level 8, n at level 2, format "''I_' n").
 
-Hint Resolve ltn_ord.
+Hint Resolve ltn_ord : core.
 
 Section OrdinalEnum.
 
diff --git a/mathcomp/ssreflect/generic_quotient.v b/mathcomp/ssreflect/generic_quotient.v
index f30c3a1..b7a8444 100644
--- a/mathcomp/ssreflect/generic_quotient.v
+++ b/mathcomp/ssreflect/generic_quotient.v
@@ -491,7 +491,7 @@ Proof. by apply: right_trans; [apply: equiv_sym|apply: equiv_trans]. Qed.
 
 End EquivRel.
 
-Hint Resolve equiv_refl.
+Hint Resolve equiv_refl : core.
 
 Notation EquivRel r er es et := (@EquivRelPack _ r (EquivClass er es et)).
 Notation "[ 'equiv_rel' 'of' e ]" := (@equiv_pack _ _ e _ id)
diff --git a/mathcomp/ssreflect/prime.v b/mathcomp/ssreflect/prime.v
index 02064c3..2a07d17 100644
--- a/mathcomp/ssreflect/prime.v
+++ b/mathcomp/ssreflect/prime.v
@@ -358,7 +358,7 @@ Proof. by case/primeP. Qed.
 Lemma prime_gt0 p : prime p -> 0 < p.
 Proof. by move/prime_gt1; apply: ltnW. Qed.
 
-Hint Resolve prime_gt1 prime_gt0.
+Hint Resolve prime_gt1 prime_gt0 : core.
 
 Lemma prod_prime_decomp n :
   n > 0 -> n = \prod_(f <- prime_decomp n) f.1 ^ f.2.
@@ -494,7 +494,7 @@ Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?pdiv_prime. Qed.
 
 Lemma max_pdiv_gt0 n : 0 < max_pdiv n.
 Proof. by case: n => [|[|n]] //; rewrite prime_gt0 ?max_pdiv_prime. Qed.
-Hint Resolve pdiv_gt0 max_pdiv_gt0.
+Hint Resolve pdiv_gt0 max_pdiv_gt0 : core.
 
 Lemma pdiv_min_dvd m d : 1 < d -> d %| m -> pdiv m <= d.
 Proof.
@@ -636,7 +636,7 @@ Proof. by rewrite lognE dvdn1 /= andbC; case: eqP => // ->. Qed.
 
 Lemma pfactor_gt0 p n : 0 < p ^ logn p n.
 Proof. by rewrite expn_gt0 lognE; case: (posnP p) => // ->. Qed.
-Hint Resolve pfactor_gt0.
+Hint Resolve pfactor_gt0 : core.
 
 Lemma pfactor_dvdn p n m : prime p -> m > 0 -> (p ^ n %| m) = (n <= logn p m).
 Proof.
@@ -858,7 +858,7 @@ Qed.
 
 Lemma part_gt0 pi n : 0 < n`_pi.
 Proof. exact: prodn_gt0. Qed.
-Hint Resolve part_gt0.
+Hint Resolve part_gt0 : core.
 
 Lemma sub_in_partn pi1 pi2 n :
   {in \pi(n), {subset pi1 <= pi2}} -> n`_pi1 %| n`_pi2.
@@ -1219,7 +1219,7 @@ Lemma odd_2'nat n : odd n = 2^'.-nat n.
 Proof. by case: n => // n; rewrite p'natE // dvdn2 negbK. Qed.
 
 End PnatTheory.
-Hint Resolve part_gt0.
+Hint Resolve part_gt0 : core.
 
 (************************************)
 (* Properties of the divisors list. *)
diff --git a/mathcomp/ssreflect/seq.v b/mathcomp/ssreflect/seq.v
index ba1f969..2c9fd64 100644
--- a/mathcomp/ssreflect/seq.v
+++ b/mathcomp/ssreflect/seq.v
@@ -1422,7 +1422,7 @@ Qed.
 
 Lemma perm_eq_refl s : perm_eq s s.
 Proof. exact/perm_eqP. Qed.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
 
 Lemma perm_eq_sym : symmetric perm_eq.
 Proof. by move=> s1 s2; apply/perm_eqP/perm_eqP=> ? ?. Qed.
@@ -1601,7 +1601,7 @@ Arguments perm_eqP {T s1 s2}.
 Arguments perm_eqlP {T s1 s2}.
 Arguments perm_eqrP {T s1 s2}.
 Prenex Implicits perm_eq.
-Hint Resolve perm_eq_refl.
+Hint Resolve perm_eq_refl : core.
 
 Section RotrLemmas.
 
@@ -1827,7 +1827,7 @@ Qed.
 
 Lemma subseq_refl s : subseq s s.
 Proof. by elim: s => //= x s IHs; rewrite eqxx. Qed.
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
 
 Lemma cat_subseq s1 s2 s3 s4 :
   subseq s1 s3 -> subseq s2 s4 -> subseq (s1 ++ s2) (s3 ++ s4).
@@ -1876,7 +1876,7 @@ End Subseq.
 Prenex Implicits subseq.
 Arguments subseqP {T s1 s2}.
 
-Hint Resolve subseq_refl.
+Hint Resolve subseq_refl : core.
 
 Section Rem.
 
diff --git a/mathcomp/ssreflect/ssrnat.v b/mathcomp/ssreflect/ssrnat.v
index b8388f0..581a7ee 100644
--- a/mathcomp/ssreflect/ssrnat.v
+++ b/mathcomp/ssreflect/ssrnat.v
@@ -316,11 +316,11 @@ Lemma leq0n n : 0 <= n.                 Proof. by []. Qed.
 Lemma ltn0Sn n : 0 < n.+1.              Proof. by []. Qed.
 Lemma ltn0 n : n < 0 = false.           Proof. by []. Qed.
 Lemma leqnn n : n <= n.                 Proof. by elim: n. Qed.
-Hint Resolve leqnn.
+Hint Resolve leqnn : core.
 Lemma ltnSn n : n < n.+1.               Proof. by []. Qed.
 Lemma eq_leq m n : m = n -> m <= n.     Proof. by move->. Qed.
 Lemma leqnSn n : n <= n.+1.             Proof. by elim: n. Qed.
-Hint Resolve leqnSn.
+Hint Resolve leqnSn : core.
 Lemma leq_pred n : n.-1 <= n.           Proof. by case: n => /=. Qed.
 Lemma leqSpred n : n <= n.-1.+1.        Proof. by case: n => /=. Qed.
 
@@ -344,7 +344,7 @@ Lemma lt0n n : (0 < n) = (n != 0).             Proof. by case: n. Qed.
 Lemma lt0n_neq0 n : 0 < n -> n != 0.           Proof. by case: n. Qed.
 Lemma eqn0Ngt n : (n == 0) = ~~ (n > 0).       Proof. by case: n. Qed.
 Lemma neq0_lt0n n : (n == 0) = false -> 0 < n. Proof. by case: n. Qed.
-Hint Resolve lt0n_neq0 neq0_lt0n.
+Hint Resolve lt0n_neq0 neq0_lt0n : core.
 
 Lemma eqn_leq m n : (m == n) = (m <= n <= m).
 Proof. by elim: m n => [|m IHm] []. Qed.
@@ -375,7 +375,7 @@ Proof. by move=> Hmn; apply: leq_trans. Qed.
 
 Lemma ltnW m n : m < n -> m <= n.
 Proof. exact: leq_trans. Qed.
-Hint Resolve ltnW.
+Hint Resolve ltnW : core.
 
 Lemma leqW m n : m <= n -> m <= n.+1.
 Proof. by move=> le_mn; apply: ltnW. Qed.