unfocus can be performed also if all goals are closed

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 1cedd2d3d3107325c363cbc29d6ee17ad3fc8c89..366a9fe16f61ce3666767bec64cc3985ee69e648 100644 (file)
--- 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
 ;;