Merge pull request #431 from ppedrot/rm-constr-hint-decls

Remove hint declarations using non-global definitions.
math-comp · Apr 9, 2020 · fea81ec · fea81ec
2 parents ad82c5f + 107954c
commit fea81ec
Show file tree

Hide file tree

Showing 4 changed files with 10 additions and 4 deletions.
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
@@ -901,7 +901,10 @@ 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) : core.
+Let integral0_RtoK := integral0 RtoK.
+Let integral1_RtoK := integral1 RtoK.
+Let monicXsubC_K := @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/field/algC.v b/mathcomp/field/algC.v
@@ -610,7 +610,8 @@ 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) : core.
+Let intr_inj_ZtoC := (intr_inj : injective ZtoC).
+Local Hint Resolve intr_inj_ZtoC : core.
 
 (* Specialization of a few basic ssrnum order lemmas. *)
 

diff --git a/mathcomp/field/algnum.v b/mathcomp/field/algnum.v
@@ -53,7 +53,8 @@ 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) : core.
+Local Definition intr_inj_ZtoC := (intr_inj : injective ZtoC).
+Local Hint Resolve intr_inj_ZtoC : core.
 Local Notation QtoCm := [rmorphism of QtoC].
 
 (* Number fields and rational spans. *)

diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
@@ -116,7 +116,8 @@ 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]) : core.
+Let intr_inj_algC := @intr_inj [numDomainType of algC].
+Local Hint Resolve intr_inj_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}.