diff options
| author | Pierre-Marie Pédrot | 2019-11-17 13:14:11 +0100 |
|---|---|---|
| committer | Reynald Affeldt | 2020-04-08 00:13:38 +0900 |
| commit | 107954c7161e95f39c266fa7b9c2fa8d2498d724 (patch) | |
| tree | 77eae20e8ed1263e1a32c3a1b87edc868bbb9680 /mathcomp/field/algC.v | |
| parent | 80d009e290eb5f935bcd4e341011bc6c5ea61531 (diff) | |
Remove hint declarations using non-global definitions.
Diffstat (limited to 'mathcomp/field/algC.v')
| -rw-r--r-- | mathcomp/field/algC.v | 3 |
1 files changed, 2 insertions, 1 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. *) |