From 667f650daefa0142eb4a2db40bcab6224947ba5a Mon Sep 17 00:00:00 2001
From: pboutill
Date: Fri, 18 Jan 2013 15:21:05 +0000
Subject: Evarconv: Check stack before term in Canonical Structure approuval

3 days of work to swap 2 lines ... but this fixes LemmaOverloading
(and hopfully makes Feit-Thomson compilation time back to "normal")

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16130 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/evarconv.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 614f99ee86..8e84d799b4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -535,15 +535,15 @@ and conv_record trs env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2))
   in
   ise_and evd'
     [(fun i ->
-       ise_list2 i
-         (fun i' x1 x -> evar_conv_x trs env i' CONV x1 (substl ks x))
-         params1 params);
-    (fun i ->
       ise_list2 i
-        (fun i' u1 u -> evar_conv_x trs env i' CONV u1 (substl ks u))
-        us2 us);
-    (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))));
-    (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1)]
+        (fun i' x1 x -> evar_conv_x trs env i' CONV x1 (substl ks x))
+        params1 params);
+     (fun i ->
+       ise_list2 i
+         (fun i' u1 u -> evar_conv_x trs env i' CONV u1 (substl ks u))
+         us2 us);
+     (fun i -> exact_ise_stack2 env i (evar_conv_x trs) ts ts1);
+     (fun i -> evar_conv_x trs env i CONV c1 (applist (c,(List.rev ks))))]
 
 (* getting rid of the optional argument rhs_is_already_stuck *)
 let evar_eqappr_x ts env evd pbty appr1 appr2 =
-- 
cgit v1.2.3