]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/tactics/variousTactics.ml
New handling of substitution:
[helm.git] / helm / ocaml / tactics / variousTactics.ml
index 0566564dc276c863954bf4c43facd662ad5f7223..ccbf6c63c92d5412040e5ead5c1a28a265e71381 100644 (file)
@@ -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 ->