Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now

processed from right to left to make the cases tactic open goals in the
expected order.

diff --git a/components/cic_unification/cicRefine.ml b/components/cic_unification/cicRefine.ml
index 9cb0a04a43b8c5c55c34a224248e078f73f8f9ce..6d26a868b10e956267954ccfe1b9d0029d08f235 100644 (file)
--- a/components/cic_unification/cicRefine.ml
+++ b/components/cic_unification/cicRefine.ml
@@ -705,8 +705,8 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
              (* TODO: check if the sort elimination 
               * is allowed: [(I q1 ... qr)|B] *)
            let (pl',_,outtypeinstances,subst,metasenv,ugraph4) =
-             List.fold_left
-               (fun (pl,j,outtypeinstances,subst,metasenv,ugraph) p ->
+             List.fold_right
+               (fun p (pl,j,outtypeinstances,subst,metasenv,ugraph) ->
                   let constructor =
                     if left_args = [] then
                       (C.MutConstruct (uri,i,j,exp_named_subst))
@@ -724,9 +724,9 @@ and type_of_aux' ?(localization_tbl = Cic.CicHash.create 1) metasenv context t
                     check_branch 0 context metasenv subst no_left_params 
                       actual_type constructor' expected_type ugraph2 
                   in
-                    (pl @ [p'],j+1,
-                     outtypeinstance::outtypeinstances,subst,metasenv,ugraph3))
-               ([],1,[],subst,metasenv,ugraph3) pl 
+                    (p'::pl,j-1,
+                     outtypeinstances@[outtypeinstance],subst,metasenv,ugraph3))
+               pl ([],List.length pl,[],subst,metasenv,ugraph3)
            in
            
              (* we are left to check that the outype matches his instances.