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

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index bd7f72e70..6aba5a993 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -272,10 +272,9 @@ let _ =
           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;
-                NRstatus.dump = fun x -> x
+               NRstatus.uhint_db = NCicUnifHint.empty_db; 
+               NRstatus.coerc_db = NCicCoercion.empty_db;
+               NRstatus.library_db = NCicLibrary.time0
             } in 
             let metasenv, subst, bo, infty = 
               NCicRefiner.typeof rdb [] [] [] bo None