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
prerr_endline "VECCHIO";
prerr_endline (CicPp.ppobj o);
let l = OCic2NCic.convert_obj u o in
+ (* fill the new env *)
+ let _ = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in
prerr_endline "OGGETTI:.........................................";
List.iter (fun o -> prerr_endline (NCicPp.ppobj o)) l;
prerr_endline "/OGGETTI:.........................................";