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

diff --git a/helm/software/components/ng_tactics/nnAuto.ml b/helm/software/components/ng_tactics/nnAuto.ml
index 2a221a213..7c52a7f72 100644
--- a/helm/software/components/ng_tactics/nnAuto.ml
+++ b/helm/software/components/ng_tactics/nnAuto.ml
@@ -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