From 941dcd389bce3e0df96281e32238010cd758999a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 7 Oct 2009 13:34:17 +0000 Subject: [PATCH] unfocus can be performed also if all goals are closed --- helm/software/components/ng_tactics/nTactics.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml index 1cedd2d3d..366a9fe16 100644 --- a/helm/software/components/ng_tactics/nTactics.ml +++ b/helm/software/components/ng_tactics/nTactics.ml @@ -153,8 +153,9 @@ let unfocus_tac status = let gstatus = match status#stack with | [] -> assert false - | ([], [], [], `FocusTag) :: s -> s - | _ -> fail (lazy "can't unfocus, some goals are still open") + | (g, [], [], `FocusTag) :: s when filter_open g = [] -> s + | _ as s -> fail (lazy ("can't unfocus, some goals are still open:\n"^ + Continuationals.Stack.pp s)) in status#set_stack gstatus ;; -- 2.39.2