From 107954c7161e95f39c266fa7b9c2fa8d2498d724 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 17 Nov 2019 13:14:11 +0100
Subject: Remove hint declarations using non-global definitions.

---
 mathcomp/algebra/mxpoly.v | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

(limited to 'mathcomp/algebra')

diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v
index b39f600..4c97dfc 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 :
-- 
cgit v1.2.3