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

diff --git a/helm/software/components/ng_refiner/check.ml b/helm/software/components/ng_refiner/check.ml
index 4e85f9bae..e039f1129 100644
--- 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