X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=f544d8daeed54aad2216322cc09f344e6bfacfa8;hb=ddc73f8ac2a7271176d3c0885c3ca1ce7638b816;hp=6aba5a993e76ded2157c689c96a40a08b33e729e;hpb=f6c887944d48d718f372a57f1609f3d059908aa8;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 6aba5a993..f544d8dae 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -187,7 +187,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 
     | NCicTypeChecker.AssertFailure s 
     | NCicTypeChecker.TypeCheckerFailure s
@@ -271,11 +271,7 @@ let _ =
           prerr_endline ("start: " ^ NUri.string_of_uri u);
           let bo = curryfy [] bo in
           (try 
-            let rdb = { 
-               NRstatus.uhint_db = NCicUnifHint.empty_db; 
-               NRstatus.coerc_db = NCicCoercion.empty_db;
-               NRstatus.library_db = NCicLibrary.time0
-            } in 
+            let rdb = new NRstatus.status in
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None
             in