From 7e1dce0f8b5116cf3eba7876c54282052faf11ba Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sat, 19 Apr 2008 16:32:36 +0000 Subject: [PATCH] impredicative set work around --- helm/software/components/ng_kernel/rt.ml | 1 + 1 file changed, 1 insertion(+) 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 -- 2.39.2