- NCicPp.ppterm applies the substitution

[helm.git] / helm / software / components / ng_kernel / check.ml

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index c1ce4260794ce9bb4388dc6a3f756f34eaa2ab5b..a61e6a8ffb0fec4a289ccb6c078a9e17cdd33d7b 100644 (file)
--- 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