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/algebra | |
| 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/algebra')
| -rw-r--r-- | mathcomp/algebra/mxpoly.v | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/mathcomp/algebra/mxpoly.v b/mathcomp/algebra/mxpoly.v index b39f600..4c97dfc 100644 --- a/mathcomp/algebra/mxpoly.v +++ b/mathcomp/algebra/mxpoly.v @@ -901,7 +901,10 @@ apply: integral_horner_root mon_p pu0 intRp _. by apply/integral_poly => i; rewrite coefX; apply: integral_nat. Qed. -Hint Resolve (integral0 RtoK) (integral1 RtoK) (@monicXsubC K) : core. +Let integral0_RtoK := integral0 RtoK. +Let integral1_RtoK := integral1 RtoK. +Let monicXsubC_K := @monicXsubC K. +Hint Resolve integral0_RtoK integral1_RtoK monicXsubC_K : core. Let XsubC0 (u : K) : root ('X - u%:P) u. Proof. by rewrite root_XsubC. Qed. Let intR_XsubC u : |