From 797a122af3ff4a9682bf77a0fb05ecfb0f9effde Mon Sep 17 00:00:00 2001 From: Andrea Asperti 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