From 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Tue, 9 Jun 2020 01:16:56 +0200
Subject: fix coq 8.12 warnings

---
 mathcomp/field/cyclotomic.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'mathcomp/field')

diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index ce8c5b7..658258c 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -117,7 +117,7 @@ Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
 
 Local Definition algC_intr_inj := @intr_inj [numDomainType of algC].
-Local Hint Resolve algC_intr_inj.
+Local Hint Resolve algC_intr_inj : 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}.
-- 
cgit v1.2.3