X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=2ab8185ab0e2e4725efb8f5eee309bf74852ab7c;hb=421056da7b3e1d6b9d91d72092b4f3c3232a00ce;hp=e039f11292923a8bbe98f6ddddfd387f8819388e;hpb=e898ca2563cc4dfbd328efc7aa3a4ff86feaec92;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index e039f1129..2ab8185ab 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -271,14 +271,13 @@ let _ =
           prerr_endline ("start: " ^ NUri.string_of_uri u);
           let bo = curryfy [] bo in
           (try 
+            let rdb = new NRstatus.status in
             let metasenv, subst, bo, infty = 
-              NCicRefiner.typeof 
-                ~look_for_coercion:(fun _ _ _ _ _ -> [])
-               NCicUnifHint.empty_db  [] [] [] bo None
+              NCicRefiner.typeof rdb [] [] [] bo None
             in
             let metasenv, subst = 
               try 
-                NCicUnification.unify NCicUnifHint.empty_db metasenv subst [] infty ty
+                NCicUnification.unify rdb metasenv subst [] infty ty
               with
               | NCicUnification.Uncertain msg 
               | NCicUnification.UnificationFailure msg