unification:

[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 7fbb781df0eff98e37a683788db4da372b5965c7..e039f11292923a8bbe98f6ddddfd387f8819388e 100644 (file)
--- a/helm/software/components/ng_refiner/check.ml
+++ b/helm/software/components/ng_refiner/check.ml
@@ -193,7 +193,7 @@ let _ =
     | 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