From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 24 May 2008 10:32:53 +0000 (+0000)
Subject: order of goals changes, open ones are preferred to closed ones as in the paper
X-Git-Tag: make_still_working~5135
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78ab40460460f98d294365543659fe3cafe7503d;p=helm.git

order of goals changes, open ones are preferred to closed ones as in the paper
---

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