X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=a61e6a8ffb0fec4a289ccb6c078a9e17cdd33d7b;hb=4257ad7d31bc2db6c40ad55878f190963e51c1ec;hp=c1ce4260794ce9bb4388dc6a3f756f34eaa2ab5b;hpb=ba51bf0b8c39758349299db24e31785acaf3ac51;p=helm.git

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index c1ce42607..a61e6a8ff 100644
--- a/helm/software/components/ng_kernel/check.ml
+++ b/helm/software/components/ng_kernel/check.ml
@@ -73,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