diff options
| author | affeldt-aist | 2020-04-09 14:10:18 +0200 |
|---|---|---|
| committer | GitHub | 2020-04-09 14:10:18 +0200 |
| commit | fea81ec06b1c309852c4c4062f4c5d1755c738d0 (patch) | |
| tree | 226b5fae28e8f58b19e58183b5a15a5b450f36d1 /mathcomp/field | |
| parent | ad82c5fb56113bdef57e96f6a79000a29803eb38 (diff) | |
| parent | 107954c7161e95f39c266fa7b9c2fa8d2498d724 (diff) | |
Merge pull request #431 from ppedrot/rm-constr-hint-decls
Remove hint declarations using non-global definitions.
Diffstat (limited to 'mathcomp/field')
| -rw-r--r-- | mathcomp/field/algC.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/algnum.v | 3 | ||||
| -rw-r--r-- | mathcomp/field/cyclotomic.v | 3 |
3 files changed, 6 insertions, 3 deletions
diff --git a/mathcomp/field/algC.v b/mathcomp/field/algC.v index 4932148..cd0a886 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 ad02f44..997255b 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 6e7432f..52472a6 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}. |