X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FvariousTactics.ml;h=d89f702fc071cb3fb732be9bba8bee5a4c2dd680;hb=fd648e40eb2c9c5b29cfa4408459511a74898d1d;hp=0566564dc276c863954bf4c43facd662ad5f7223;hpb=655906d74521fa49de332f54ec34bfc9d9744151;p=helm.git

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index 0566564dc..d89f702fc 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -220,11 +220,13 @@ let rec auto_new mqi_handle = function
 
 
 let auto_tac mqi_handle =
+(*   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";
+    prerr_endline "AUTO_TAC HA FINITO";
+(*     CicMetaSubst.print_counters (); *)
     (proof,[])
   with 
   | NoOtherChoices ->