From 6bfc094b858c7ab1c5df7f780d68e04ba0ba4c23 Mon Sep 17 00:00:00 2001
From: Cyril Cohen
Date: Mon, 8 Jun 2020 17:27:57 +0200
Subject: turning let into local definition

---
 mathcomp/field/cyclotomic.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/field/cyclotomic.v b/mathcomp/field/cyclotomic.v
index 52472a6..ce8c5b7 100644
--- a/mathcomp/field/cyclotomic.v
+++ b/mathcomp/field/cyclotomic.v
@@ -116,8 +116,8 @@ Local Notation pZtoQ := (map_poly ZtoQ).
 Local Notation pZtoC := (map_poly ZtoC).
 Local Notation pQtoC := (map_poly ratr).
 
-Let intr_inj_algC := @intr_inj [numDomainType of algC].
-Local Hint Resolve intr_inj_algC : core.
+Local Definition algC_intr_inj := @intr_inj [numDomainType of algC].
+Local Hint Resolve algC_intr_inj.
 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