From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 30 Jan 2007 13:42:09 +0000 (+0000)
Subject: Behaviour of CicRefine.type_of_aux' on MutCases changed: branches are now
X-Git-Tag: make_still_working~6500
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;ds=sidebyside;h=0978a9c19e672bb0b505f25737078409381700c7;p=helm.git

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/helm/software/components/cic_unification/cicRefine.ml b/helm/software/components/cic_unification/cicRefine.ml
index 9cb0a04a4..6d26a868b 100644
--- a/helm/software/components/cic_unification/cicRefine.ml
+++ b/helm/software/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.