Merge pull request #79 from proux01/coq_16004

Adapt to coq/coq#16004

theories/abel.v

@@ -824,7 +824,7 @@ Proof. by rewrite /numfield; case: splitting_num_field => //= ? [? []]. Qed.
 
 Lemma char_numfield (p : {poly rat}) : [char (numfield p)] =i pred0.
 Proof. exact: char_ext. Qed.
-Hint Resolve char_numfield : core.
+#[global] Hint Resolve char_numfield : core.
 
 Lemma normal_numfield (p : {poly rat}) : normalField 1 {: numfield p}.
 Proof.
@@ -1193,19 +1193,19 @@ Proof. by rewrite -size_poly_eq0 size_poly_example_int. Qed.
 
 Lemma poly_example_neq0 : poly_example != 0.
 Proof. by rewrite -size_poly_eq0 size_poly_example. Qed.
-Hint Resolve poly_example_neq0 : core.
+#[local] Hint Resolve poly_example_neq0 : core.
 
 Lemma poly_example_monic : poly_example \is monic.
 Proof. by rewrite monicE lead_coefE !pesimp size_poly_example. Qed.
-Hint Resolve poly_example_monic : core.
+#[local] Hint Resolve poly_example_monic : core.
 
 Lemma irreducible_example : irreducible_poly poly_example.
 Proof.
 rewrite poly_exampleEint; apply: (@eisenstein 2) => // [|||i];
   rewrite ?lead_coefE ?size_poly_example_int ?pesimp//.
 by move: i; do 6!case=> //.
 Qed.
-Hint Resolve irreducible_example : core.
+#[local] Hint Resolve irreducible_example : core.
 
 Lemma separable_example : separable_poly poly_example.
 Proof.
@@ -1216,7 +1216,7 @@ have size_deriv_example : size poly_example^`() = 5%N.
 rewrite gtNdvdp -?size_poly_eq0 ?size_deriv_example//.
 by rewrite (eqp_size eqq) ?size_poly_example.
 Qed.
-Hint Resolve separable_example : core.
+#[local] Hint Resolve separable_example : core.
 
 Lemma prime_example : prime (size poly_example).-1.
 Proof. by rewrite size_poly_example. Qed.
@@ -1255,7 +1255,7 @@ Proof.
 apply/eqP => /(congr1 (fun p => p.[0])).
 by rewrite deriv_poly_example !pesimp => /eqP; compute.
 Qed.
-Hint Resolve deriv_poly_example_neq0 : core.
+#[local] Hint Resolve deriv_poly_example_neq0 : core.
 
 Definition alpha : algR := Num.sqrt (2%:R / Num.sqrt 5%:R).
 

theories/xmathcomp/map_gal.v

@@ -358,7 +358,7 @@ rewrite -(@normalField_img _ _ E)// ?galois_normalW//.
 Qed.
 
 End Prodv.
-Hint Resolve normalField_refl : core.
+#[global] Hint Resolve normalField_refl : core.
 
 Section map_hom.
 Variables (F0 : fieldType) (L L' : splittingFieldType F0).
@@ -696,7 +696,7 @@ Lemma normalClosureSl E F : (E <= normalClosure E F)%VS.
 Proof.
 by rewrite (subv_trans (field_subvMr _ _) (prodv_sub_normalClosure _ _)).
 Qed.
-Hint Resolve normalClosureSl : core.
+#[local] Hint Resolve normalClosureSl : core.
 
 Lemma normalClosureSr E F : (F <= normalClosure E F)%VS.
 Proof. exact: subv_trans (field_subvMl _ _) (prodv_sub_normalClosure _ _). Qed.
@@ -711,7 +711,7 @@ under eq_bigr => s' do have -> : (s \o s')%VF = 'R%act s' s by [].
 have /(reindex_astabs 'R _) : s \in ('N(kAEndf E | 'R))%g by rewrite astabsR/=.
 by move/(_ _ _ _ (fun i => i @: (E * F))%AS); rewrite !big_prodv_eq_aspace => <-.
 Qed.
-Hint Resolve normalClosure_normal : core.
+#[local] Hint Resolve normalClosure_normal : core.
 
 Lemma normalClosure_separable E F : separable E F ->
    separable E (normalClosure E F).
@@ -725,7 +725,7 @@ Proof.
 move=> sepEF; rewrite /galois.
 by rewrite normalClosureSl normalClosure_separable// normalClosure_normal.
 Qed.
-Hint Resolve normalClosure_galois : core.
+#[local] Hint Resolve normalClosure_galois : core.
 
 Lemma normalClosureP E F K' : (E <= K')%VS -> (F <= K')%VS ->
   normalField E K' -> (normalClosure E F <= K')%VS.
@@ -773,7 +773,7 @@ Lemma solvable_ext_refl E : solvable_ext E E.
 Proof.
 by apply/solvable_extP; exists E; rewrite subvv galois_refl/= galvv solvable1.
 Qed.
-Hint Resolve solvable_ext_refl : core.
+#[local] Hint Resolve solvable_ext_refl : core.
 
 Lemma sub_solvable_ext F K E :
   (E <= F)%VS -> solvable_ext K F -> solvable_ext K E.
@@ -837,10 +837,10 @@ Qed.
 
 End normalClosure.
 
-Hint Resolve normalClosureSl : core.
-Hint Resolve normalClosureSr : core.
-Hint Resolve normalClosure_normal : core.
-Hint Resolve solvable_ext_refl : core.
+#[global] Hint Resolve normalClosureSl : core.
+#[global] Hint Resolve normalClosureSr : core.
+#[global] Hint Resolve normalClosure_normal : core.
+#[global] Hint Resolve solvable_ext_refl : core.
 
 Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0)
   (iota : 'AHom(L, L')) (K E : {subfield L}) :