From 797a122af3ff4a9682bf77a0fb05ecfb0f9effde Mon Sep 17 00:00:00 2001
From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 19 Feb 2010 17:15:41 +0000
Subject: [PATCH] Open goals fixed (it also returned closed goals).

---
 helm/software/components/ng_tactics/nnAuto.ml | 11 ++++++++---
 1 file changed, 8 insertions(+), 3 deletions(-)

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index c8a2c9c4a..8f3ba4921 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -1599,7 +1599,7 @@ let applicative_case depth signature status flags gty (cache:cache) =
   debug_print ~depth
     (lazy ("smart candidates: " ^ 
              string_of_int (List.length smart_candidates)));
-(*
+ (*
   let sm = 0 in 
   let smart_candidates = [] in *)
   let sm = if is_eq then 0 else 2 in
@@ -1875,12 +1875,17 @@ let deep_focus_tac level focus status =
    status#set_stack gstatus
 ;;
 
-let open_goals level status = 
+let open_goals level status =
   let rec aux level gs = 
     if level = 0 then []
     else match gs with 
       | [] -> assert false
-      | _ :: s -> head_goals gs @ aux (level-1) s
+      | (g, _, _, _) :: s -> 
+          let is_open = function
+           | (_,Continuationals.Stack.Open i) -> Some i
+           | (_,Continuationals.Stack.Closed _) -> None
+          in
+	    HExtlib.filter_map is_open g @ aux (level-1) s
   in
   aux level status#stack
 ;;
-- 
2.39.2