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 fabfcf4de2c961dbdb57e0cb81fb4f0b2006401c..37f0939bd16e447e48d6420514ed5537b8d26c1f 100644 (file)
--- 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