Printings removed.

diff --git a/helm/software/components/ng_tactics/.depend b/helm/software/components/ng_tactics/.depend
index 587b29a3aa997b8d8d8d1613d62bb9c5e1345eb4..5698bbd5f3fbeb84216ddb7971d509f659a614df 100644 (file)
--- 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 2a221a21331519f40253f16f103c5194e312af37..7c52a7f72ebf7f0122acc2d8f20f4500d2cc0605 100644 (file)
--- 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