X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=f5fb6841c39a47efdc878408a1eb5a20f7f9deea;hb=4ae18461e6dfbf0011c062ab56fe85be00f011ec;hp=d10b771aad2b249618ba4178db18ceba1cd955a6;hpb=a4086666ce84a0a71a587cafd52d1a08b26e54f0;p=helm.git diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml index d10b771aa..f5fb6841c 100644 --- a/helm/software/components/ng_kernel/check.ml +++ b/helm/software/components/ng_kernel/check.ml @@ -176,7 +176,7 @@ let _ = let o = NCicLibrary.get_obj uu in if print_object then prerr_endline (NCicPp.ppobj o); try - NCicTypeChecker.typecheck_obj o + NCicEnvironment.check_and_add_obj o with exn -> let rec aux = function @@ -204,9 +204,9 @@ let _ = let prima = Unix.gettimeofday () in List.iter (fun u -> - let u= OCic2NCic.nuri_of_ouri u in + let u= OCic2NCic.nuri_of_ouri u in indent := 0; - NCicTypeChecker.typecheck_obj (NCicLibrary.get_obj u)) + ignore (NCicEnvironment.get_checked_obj u)) alluris; let dopo = Unix.gettimeofday () in Gc.compact ();