From 95b2fec522138b2a17e6f8ddc71683eb9dbf3413 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Tue, 23 Nov 2010 14:06:30 +0000 Subject: [PATCH] Debugging code commented out. --- helm/software/components/ng_tactics/nnAuto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml index 344e7535c..7a9c20f0f 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -1740,7 +1740,7 @@ let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status = oldstatus#set_status s in let s = up_to depth depth in - print (print_stat statistics); + debug_print (print_stat statistics); debug_print(lazy ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time))); debug_print(lazy -- 2.39.2