EXPERIMENTAL COMMIT (by CSC,actuall :-)

[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 51f0482a525825451ec729a0f9ac14aad34929f8..bd7f72e70b1d3040448f71290e097fc5a54f0964 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -273,7 +273,9 @@ let _ =
           (try 
             let rdb = { 
                 NRstatus.uhint_db = NCicUnifHint.empty_db; 
-                NRstatus.coerc_db = NCicCoercion.empty_db 
+                NRstatus.coerc_db = NCicCoercion.empty_db;
+                NRstatus.library_db = NCicLibrary.time0;
+                NRstatus.dump = fun x -> x
             } in 
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None