From 107954c7161e95f39c266fa7b9c2fa8d2498d724 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Pierre-Marie=20P=C3=A9drot?= Date: Sun, 17 Nov 2019 13:14:11 +0100 Subject: [PATCH] Remove hint declarations using non-global definitions. --- mathcomp/algebra/mxpoly.v | 5 ++++- mathcomp/field/algC.v | 3 ++- mathcomp/field/algnum.v | 3 ++- mathcomp/field/cyclotomic.v | 3 ++- 4 files changed, 10 insertions(+), 4 deletions(-) diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b39f6007c9..4c97dfcf0e 100644 --- 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 index 4932148abb..cd0a88613e 100644 --- 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 index 15d1d61c87..c87b55c5f0 100644 --- 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 index 6e7432f7af..52472a6405 100644 --- 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}.