Initial implementation of statuses using objects in place of nested records.

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

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 6aba5a993e76ded2157c689c96a40a08b33e729e..2ab8185ab0e2e4725efb8f5eee309bf74852ab7c 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -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