From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 5 Jul 2004 07:04:13 +0000 (+0000)
Subject: commented out some debugging instructions
X-Git-Tag: pre_subst_in_kernel~8
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=48afaef59db6831345f7a13bd0d66a2c06bc2b80;p=helm.git

commented out some debugging instructions
---

diff --git a/helm/ocaml/tactics/variousTactics.ml b/helm/ocaml/tactics/variousTactics.ml
index ccbf6c63c..d89f702fc 100644
--- a/helm/ocaml/tactics/variousTactics.ml
+++ b/helm/ocaml/tactics/variousTactics.ml
@@ -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 ->