- added (hack) apply_tac_verbose (for auto)

[helm.git] / helm / ocaml / tactics / variousTactics.ml

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index ccbf6c63c92d5412040e5ead5c1a28a265e71381..9293d14399756c7eb5ee677982700f42b819f16c 100644 (file)
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -220,14 +220,16 @@ let rec auto_new mqi_handle = function
 
 
 let auto_tac mqi_handle =
-  CicMetaSubst.reset_counters ();
+(*   CicMetaSubst.reset_counters (); *)
  let auto_tac mqi_handle (proof,goal) =
   prerr_endline "Entro in Auto";
   try 
-    let (proof,_)::_ = auto_new mqi_handle [(proof, [(goal,depth)])] in
-    prerr_endline "AUTO_TAC HA FINITO";
-    CicMetaSubst.print_counters ();
-    (proof,[])
+    (match auto_new mqi_handle [(proof, [(goal,depth)])] with
+    | (proof,_)::_  ->
+      prerr_endline "AUTO_TAC HA FINITO";
+  (*     CicMetaSubst.print_counters (); *)
+      (proof,[])
+    | _ -> assert false)
   with 
   | NoOtherChoices ->
       prerr_endline("Auto failed");