2 NCicTypeChecker.set_logger
4 | `Start_type_checking s ->
5 prerr_endline ("Start: " ^ NUri.string_of_uri s)
6 | `Type_checking_completed s ->
7 prerr_endline ("End: " ^ NUri.string_of_uri s));
8 NCicPp.set_ppterm NCicPp.trivial_pp_term;
9 Helm_registry.load_from "conf.xml";
10 let u = UriManager.uri_of_string Sys.argv.(1) in
11 let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
12 let l = OCic2NCic.convert_obj u o in
14 (fun (u,_,_,_,_ as o) ->
15 prerr_endline ("CHECK: " ^ NUri.string_of_uri u ^"\n"^NCicPp.ppobj o);
16 try NCicTypeChecker.typecheck_obj o
18 | NCicTypeChecker.AssertFailure s
19 | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s)
20 (*| CicEnvironment.Object_not_found s ->
21 prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)*))