X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;fp=helm%2Fsoftware%2Fcomponents%2Fng_kernel%2Fcheck.ml;h=f5fb6841c39a47efdc878408a1eb5a20f7f9deea;hb=bd1e80fb01cfb419e256d5899ac5bf8818f11e64;hp=d10b771aad2b249618ba4178db18ceba1cd955a6;hpb=8863adcc7dc67d3f4f6ba96c2424698cd6b21446;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 ();