diff options
| author | Cyril Cohen | 2020-06-09 01:16:56 +0200 |
|---|---|---|
| committer | Cyril Cohen | 2020-06-09 04:45:15 +0200 |
| commit | 8006cbf40eeb017aacb3ecaa8c4538f9a5aaa3bf (patch) | |
| tree | 805fe2e3ff31c9741ae0ded3cd7ab24b7068f60d /mathcomp/field | |
| parent | 6784363d60493b8ec154bbf1e827ec677d6b5921 (diff) | |
fix coq 8.12 warnings
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 2 |
1 files changed, 1 insertions, 1 deletions
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}. |