change in the order of unification constraints solving (for canonical structures)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12223 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 6 insertions, 6 deletions

diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d6b10b7d0..272225aca 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -482,15 +482,15 @@ and conv_record env evd (c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
   in
   ise_and evd'
     [(fun i ->
-      ise_list2 i
-        (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
-        us2 us);
-     (fun i ->
        ise_list2 i
          (fun i x1 x -> evar_conv_x env i CONV x1 (substl ks x))
          params1 params);
-     (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1);
-     (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))))]
+    (fun i ->
+      ise_list2 i
+        (fun i u1 u -> evar_conv_x env i CONV u1 (substl ks u))
+        us2 us);
+    (fun i -> evar_conv_x env i CONV c1 (applist (c,(List.rev ks))));
+    (fun i -> ise_list2 i (fun i -> evar_conv_x env i CONV) ts ts1)]
 
 (* We assume here |l1| <= |l2| *)