X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2Fcheck.ml;h=f544d8daeed54aad2216322cc09f344e6bfacfa8;hb=c22f39a5d5afc0ef55beb221e00e2e6703b13d90;hp=d4a329697d667287d859b03e58150cc8d7f93a39;hpb=48794769c34c57e3ead42edc8c8eca5333e857ea;p=helm.git

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index d4a329697..f544d8dae 100644
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -187,13 +187,13 @@ let _ =
     let o = NCicLibrary.get_obj uu in
     if print_object then prerr_endline (NCicPp.ppobj o); 
     try 
-      NCicTypeChecker.typecheck_obj o
+      NCicEnvironment.check_and_add_obj o
     with 
     | NCicTypeChecker.AssertFailure s 
     | NCicTypeChecker.TypeCheckerFailure s
     | NCicEnvironment.ObjectNotFound s
     | NCicEnvironment.BadConstraint s
-    | NCicEnvironment.BadDependency s as e -> 
+    | NCicEnvironment.BadDependency (s,_) as e -> 
        prerr_endline ("######### " ^ Lazy.force s);
        if not ignore_exc then raise e
     )
@@ -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,12 +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 [] [] [] bo None
+              NCicRefiner.typeof rdb [] [] [] bo None
             in
             let metasenv, subst = 
               try 
-                NCicUnification.unify metasenv subst [] infty ty
+                NCicUnification.unify rdb metasenv subst [] infty ty
               with
               | NCicUnification.Uncertain msg 
               | NCicUnification.UnificationFailure msg