From 1eaf58f3b0f2f7a871f627bcea36c8d04d8309e2 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Thu, 18 Mar 2010 11:28:22 +0000 Subject: [PATCH] Debugging disabled. --- 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 f314d3eb3..2a221a213 100644 --- a/helm/software/components/ng_tactics/nnAuto.ml +++ b/helm/software/components/ng_tactics/nnAuto.ml @@ -172,7 +172,7 @@ let solve f status eq_cache goal = let gty = NCicUntrusted.apply_subst subst ctx gty in let build_status (pt, _, metasenv, subst) = try - print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt))); + debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt))); let stamp = Unix.gettimeofday () in let metasenv, subst, pt, pty = (* NCicRefiner.typeof status -- 2.39.2