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 c8a2c9c4a6b74ffbd255eeea2296124114473af6..8f3ba4921dac1568399c076ce9e7442181efb29c 100644 (file)
--- 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
 ;;