From 78ab40460460f98d294365543659fe3cafe7503d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
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.5