From ad931e65a902120e96b9ec47f264015db033135d Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Sat, 12 Dec 2015 18:34:15 +0100
Subject: Revert "HACK: work around regression in 8.5"

This reverts commit 006565bdb5b473afff5f834e4b20320bb0a419fd.
since Coq commit c6b75e1b693ab8c7af2efd1b93f04eab248e584c
make this unnecessary
---
 mathcomp/field/finfield.v | 14 +-------------
 1 file changed, 1 insertion(+), 13 deletions(-)

(limited to 'mathcomp/field')

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.
-- 
cgit v1.2.3