diff options
| author | Enrico Tassi | 2015-12-12 18:34:15 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-12-12 18:34:15 +0100 |
| commit | ad931e65a902120e96b9ec47f264015db033135d (patch) | |
| tree | bb15b11f74fe42c0391f42eacdbfb893521b95ef /mathcomp | |
| parent | 353eb61703f64f6d0f520720fdb0d08a1cf727c3 (diff) | |
Revert "HACK: work around regression in 8.5"
This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd.
since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c
make this unnecessary
Diffstat (limited to 'mathcomp')
| -rw-r--r-- | mathcomp/field/finfield.v | 14 |
1 files changed, 1 insertions, 13 deletions
diff --git a/mathcomp/field/finfield.v b/mathcomp/field/finfield.v index 88f2570..ebf69e7 100644 --- a/mathcomp/field/finfield.v +++ b/mathcomp/field/finfield.v @@ -529,19 +529,7 @@ have [L [zs Dq]]: {L : fieldExtType K & splits L q^%:A}. apply: (IHn (FinFieldExtType K) q nz_q). by rewrite ltnS Dszp size_mul ?polyXsubC_eq0 ?size_XsubC ?addn2 in lbn. suffices: splits L p^%:A^%:A. - (* Work around: the extra args to baseField_scaleE avoid divergence. - - If you "Check (fun a => baseField_scaleE a 1)" it gives a result that contains 3 - unresolved evars. - The last one looks like "?t : [ ... x: ?t |- fieldType ] (x cannot be used)", so - pruning avoids cyclicity. - - Doing a "Check ((fun a => baseField_scaleE a 1) : _)" shows the divergence. - - Divergence (stack overflow) happens in occur_evar_upto_types, but a quick look - shows that the functions it calls do honor the filter (pruning). - *) - rewrite -[_^%:A]map_poly_comp -(eq_map_poly (fun a => @baseField_scaleE F K _ a 1)). + rewrite -[_^%:A]map_poly_comp -(eq_map_poly (fun a => baseField_scaleE a 1)). by exists [fieldExtType F of baseFieldType L]. exists (x%:A :: zs); rewrite big_cons; set rhs := _ * _. by rewrite Dp mulrC [_^%:A]rmorphM /= mapXsubC /= eqp_mull. |