From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Thu, 18 Mar 2010 11:33:10 +0000 (+0000)
Subject: Printings removed.
X-Git-Tag: make_still_working~2989
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=63047f8ff8ef477ac32939985b0b41b70e918054;p=helm.git

Printings removed.
---

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 587b29a3a..5698bbd5f 100644
--- a/helm/software/components/ng_tactics/.depend
+++ b/helm/software/components/ng_tactics/.depend
@@ -1,4 +1,8 @@
+nCicTacReduction.cmi: 
+nTacStatus.cmi: 
+nCicElim.cmi: 
 nTactics.cmi: nTacStatus.cmi 
+zipTree.cmi: 
 andOrTree.cmi: zipTree.cmi 
 nnAuto.cmi: nTacStatus.cmi 
 nAuto.cmi: nTacStatus.cmi 
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