From 78ab40460460f98d294365543659fe3cafe7503d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 24 May 2008 10:32:53 +0000 Subject: [PATCH] order of goals changes, open ones are preferred to closed ones as in the paper --- helm/software/components/tactics/auto.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml index fabfcf4de..37f0939bd 100644 --- a/helm/software/components/tactics/auto.ml +++ b/helm/software/components/tactics/auto.ml @@ -750,10 +750,11 @@ let split_goals_with_metas metasenv subst gl = let order_new_goals metasenv subst open_goals ppterm = let prop,rest = split_goals_in_prop metasenv subst open_goals in let closed_prop, open_prop = split_goals_with_metas metasenv subst prop in + let closed_type, open_type = split_goals_with_metas metasenv subst rest in let open_goals = - (List.map (fun x -> x,P) (closed_prop @ open_prop)) + (List.map (fun x -> x,P) (open_prop @ closed_prop)) @ - (List.map (fun x -> x,T) rest) + (List.map (fun x -> x,T) (open_type @ closed_type)) in let tys = List.map -- 2.39.2