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 4e85f9bae069d64214ccb599d4d9579e6e83f62c..2ab8185ab0e2e4725efb8f5eee309bf74852ab7c 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -220,7 +220,8 @@ let _ =
             | NCic.Appl (NCic.Const (NReference.Ref (u,_))::ty::_)
               when NUri.string_of_uri u = "cic:/matita/tests/hole.con" ->
                 let metasenv, ty =  perforate ctx metasenv ty in
-                let a,b,_ = NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
+                let a,_,b,_ = 
+                  NCicMetaSubst.mk_meta metasenv ctx (`WithType ty) in a,b
             | t -> 
                 NCicUntrusted.map_term_fold_a
                  (fun e ctx -> e::ctx) ctx perforate metasenv t
@@ -270,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