X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Ftactics%2FautoTactic.ml;h=8e94bba86e4f072796f32d482f363d5df2e5ed24;hb=004ccf29097c8ab5c4997555b54aba5831fa035a;hp=cdfcf8c73ec560dfaf887bb9540e0267e4503659;hpb=470db3bb0aac5920297859373f73a70b6f38fca9;p=helm.git

diff --git a/helm/software/components/tactics/autoTactic.ml b/helm/software/components/tactics/autoTactic.ml
index cdfcf8c73..8e94bba86 100644
--- a/helm/software/components/tactics/autoTactic.ml
+++ b/helm/software/components/tactics/autoTactic.ml
@@ -286,7 +286,7 @@ let auto_tac_old ?(depth=default_depth) ?(width=default_width) ~(dbd:HMysql.dbd)
         debug_print (lazy "AUTO_TAC HA FINITO");
         let _,_,p,_ = proof in
         debug_print (lazy (CicPp.ppterm p));
-        Printf.printf "tempo: %.9f\n" (t2 -. t1);
+        debug_print (lazy (Printf.sprintf "tempo: %.9f\n" (t2 -. t1)));
         (proof,[])
     | _ -> assert false
   in