auto works on the regular tactics status

[helm.git] / helm / software / components / ng_tactics / nTactics.ml

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index 760d84e8d90bdf22157a405b30ee4d4afe0c5b51..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
 ;;
@@ -655,30 +656,3 @@ let assert_tac seqs status =
      ) status
 ;;
 
-let auto ~params:(l,_) status goal =
-  let gty = get_goalty status goal in
-  let n,h,metasenv,subst,o = status#obj in
-  let status,t = term_of_cic_term status gty (ctx_of gty) in
-  let status, l = 
-    List.fold_left
-      (fun (status, l) t ->
-        let status, t = disambiguate status t None (ctx_of gty) in
-        let status, ty = typeof status (ctx_of t) t in
-        let status, t =  term_of_cic_term status t (ctx_of gty) in
-        let status, ty = term_of_cic_term status ty (ctx_of ty) in
-        (status, (t,ty) :: l))
-      (status,[]) l
-  in
-  match
-    NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l 
-  with
-  | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
-  | (pt, metasenv, subst)::_ -> 
-      let status = status#set_obj (n,h,metasenv,subst,o) in
-      instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
-;;
-
-let auto_tac ~params status =
-  distribute_tac (auto ~params) status
-;;
-