From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 19 Feb 2010 17:15:41 +0000 (+0000)
Subject: Open goals fixed (it also returned closed goals).
X-Git-Tag: make_still_working~3032
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=797a122af3ff4a9682bf77a0fb05ecfb0f9effde;hp=93205dc852fa208b48a05757d05d9910b7d45fa1;p=helm.git

Open goals fixed (it also returned closed goals).
---

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
 ;;