From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 19 Apr 2008 16:32:36 +0000 (+0000)
Subject: impredicative set work around
X-Git-Tag: make_still_working~5308
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7e1dce0f8b5116cf3eba7876c54282052faf11ba;p=helm.git

impredicative set work around
---

diff --git a/helm/software/components/ng_kernel/rt.ml b/helm/software/components/ng_kernel/rt.ml
index cc4d5dd33..a4838a52a 100644
--- a/helm/software/components/ng_kernel/rt.ml
+++ b/helm/software/components/ng_kernel/rt.ml
@@ -1,5 +1,6 @@
 let _ =
   Helm_registry.load_from "conf.xml";
+  CicParser.impredicative_set := false;
   NCicPp.set_ppterm NCicPp.trivial_pp_term;
   let u = UriManager.uri_of_string Sys.argv.(1) in
   let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in