let _ =
  NCicTypeChecker.set_logger 
    (function 
    | `Start_type_checking s -> 
       prerr_endline ("Start: " ^ NUri.string_of_uri s)
    | `Type_checking_completed s -> 
       prerr_endline ("End: " ^ NUri.string_of_uri s));
  NCicPp.set_ppterm NCicPp.trivial_pp_term;
  Helm_registry.load_from "conf.xml";
  let u = UriManager.uri_of_string Sys.argv.(1) in
  let o, _ = CicEnvironment.get_obj CicUniv.oblivion_ugraph u in
  let l = OCic2NCic.convert_obj u o in
  List.iter 
    (fun o ->
       try NCicTypeChecker.typecheck_obj o
       with 
       | NCicTypeChecker.AssertFailure s 
       | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s))
    l
;;