X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnnAuto.ml;h=7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605;hb=ef6a409b9cea2a3d0b0852ae3e69737566c91ba1;hp=f314d3eb389dbef693107a4f518750819064583c;hpb=f1fc99e982ca6c9c939504c4dcf773edf582792a;p=helm.git

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index f314d3eb3..7c52a7f72 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
@@ -483,7 +483,6 @@ let smart_apply t unit_eq status g =
   let status,t = term_of_cic_term status t ctx in
   let _,_,metasenv,subst,_ = status#obj in
   let ty = NCicTypeChecker.typeof subst metasenv ctx t in
-  print(lazy("prima"));
   let ty,metasenv,args = 
     match gty with
       | NCic.Const(nref)
@@ -498,8 +497,8 @@ let smart_apply t unit_eq status g =
       | NCic.Appl l -> NCic.Appl(l@args) 
       | _ -> NCic.Appl(t::args) 
   in
-  print(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
-  print(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
+  noprint(lazy("pterm " ^ (NCicPp.ppterm ctx [] [] pterm)));
+  noprint(lazy("pty " ^ (NCicPp.ppterm ctx [] [] ty)));
   let eq_coerc =       
     let uri = 
       NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in