]> matita.cs.unibo.it Git - helm.git/commitdiff
unfocus can be performed also if all goals are closed
authorEnrico Tassi <enrico.tassi@inria.fr>
Wed, 7 Oct 2009 13:34:17 +0000 (13:34 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Wed, 7 Oct 2009 13:34:17 +0000 (13:34 +0000)
helm/software/components/ng_tactics/nTactics.ml

index 1cedd2d3d3107325c363cbc29d6ee17ad3fc8c89..366a9fe16f61ce3666767bec64cc3985ee69e648 100644 (file)
@@ -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
 ;;