From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Wed, 7 Oct 2009 13:34:17 +0000 (+0000)
Subject: unfocus can be performed also if all goals are closed
X-Git-Tag: make_still_working~3360
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=941dcd389bce3e0df96281e32238010cd758999a;p=helm.git

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