From 7a513418898ec932e8379e01e6feedf07566bafb Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 4 Apr 2008 17:41:58 +0000 Subject: [PATCH] fix --- helm/software/components/ng_kernel/check.ml | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index 908493cbe..a54890285 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -8,16 +8,11 @@ let _ = 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 (u,_,_,_,_ as o) -> - prerr_endline ("CHECK: " ^ NUri.string_of_uri u ^"\n"^NCicPp.ppobj o); - try NCicTypeChecker.typecheck_obj o - with - | NCicTypeChecker.AssertFailure s - | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s) - (*| CicEnvironment.Object_not_found s -> - prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s)*)) - l + let _,o = NCicEnvironment.get_obj (NUri.nuri_of_ouri u) in + try NCicTypeChecker.typecheck_obj o + with + | NCicTypeChecker.AssertFailure s + | NCicTypeChecker.TypeCheckerFailure s -> prerr_endline (Lazy.force s) + | CicEnvironment.Object_not_found s -> + prerr_endline ("Obj not found: " ^ UriManager.string_of_uri s) ;; -- 2.39.2