From 0978a9c19e672bb0b505f25737078409381700c7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 30 Jan 2007 13:42:09 +0000 Subject: [PATCH] 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. --- helm/software/components/cic_unification/cicRefine.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) 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. -- 2.39.2