From 4cc970d00483c8c2a0a26cba3296bf855be01ed7 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 30 Oct 2006 17:31:31 +0000 Subject: [PATCH] Debugging code is now controlled by the debug flag. --- helm/software/components/tactics/autoTactic.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2