X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=a61e6a8ffb0fec4a289ccb6c078a9e17cdd33d7b;hb=4a72a8de2b78b7ab0d200a4bf2f197d9ce2f2a13;hp=164e1a223c5eb1ae372ef3e9e4ec70041c98414e;hpb=f72ad4ff2fd12310fb7915f74721697b928b9aea;p=helm.git

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index 164e1a223..a61e6a8ff 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -15,6 +15,7 @@ let debug = true
 let ignore_exc = false
 let rank_all_dependencies = false
 let trust_environment = false
+let print_object = false
 
 let indent = ref 0;;
 
@@ -72,7 +73,6 @@ let _ =
       prerr_endline (HelmLogger.string_of_html_msg html_msg));
   CicParser.impredicative_set := false;
   NCicTypeChecker.set_logger logger;
-  NCicPp.set_ppterm NCicPp.trivial_pp_term;
   Helm_registry.load_from "conf.xml";
   let alluris = 
     try
@@ -173,7 +173,7 @@ let _ =
     let uu= OCic2NCic.nuri_of_ouri uu in
     indent := 0;
     let o = NCicLibrary.get_obj uu in
-       prerr_endline (NCicPp.ppobj o); 
+    if print_object then prerr_endline (NCicPp.ppobj o); 
     try 
       NCicTypeChecker.typecheck_obj o
     with