]> matita.cs.unibo.it Git - helm.git/commitdiff
commented out some debugging instructions
authorStefano Zacchiroli <zack@upsilon.cc>
Mon, 5 Jul 2004 07:04:13 +0000 (07:04 +0000)
committerStefano Zacchiroli <zack@upsilon.cc>
Mon, 5 Jul 2004 07:04:13 +0000 (07:04 +0000)
helm/ocaml/tactics/variousTactics.ml

index ccbf6c63c92d5412040e5ead5c1a28a265e71381..d89f702fc071cb3fb732be9bba8bee5a4c2dd680 100644 (file)
@@ -220,13 +220,13 @@ 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 ();
+(*     CicMetaSubst.print_counters (); *)
     (proof,[])
   with 
   | NoOtherChoices ->