1) NCicTypechecker.typecheck_obj removed, since it did not add to the

[helm.git] / helm / software / components / ng_kernel / check.ml

diff --git a/helm/software/components/ng_kernel/check.ml b/helm/software/components/ng_kernel/check.ml
index d10b771aad2b249618ba4178db18ceba1cd955a6..f5fb6841c39a47efdc878408a1eb5a20f7f9deea 100644 (file)
--- 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 ();