Fix some new warnings emitted by Coq 8.10:

```
Warning: Adding and removing hints in the core database implicitly is
deprecated. Please specify a hint database.
[implicit-core-hint-db,deprecated]
```

11 files changed, 44 insertions, 44 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}.