X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_refiner%2FnCicUnification.ml;h=0f73dbc5c9e5f0fd268010092448dbce9c5b9e48;hb=9d33fd0863f207cee7f882ae28c83e1944d2a0f1;hp=1a667770b4ec47b762c8c3d27e090310d2f16f4b;hpb=8e1b4eb6c9c8544f754b525d6cf2ba5ab0bf5396;p=helm.git

diff --git a/helm/software/components/ng_refiner/nCicUnification.ml b/helm/software/components/ng_refiner/nCicUnification.ml
index 1a667770b..0f73dbc5c 100644
--- a/helm/software/components/ng_refiner/nCicUnification.ml
+++ b/helm/software/components/ng_refiner/nCicUnification.ml
@@ -453,7 +453,7 @@ and unify rdb test_eq_only metasenv subst context t1 t2 =
              l1 l2 (metasenv, subst, [], List.length l1)
            in
            if to_restrict <> [] then
-             let metasenv, subst, _ = 
+             let metasenv, subst, _, _ = 
                NCicMetaSubst.restrict metasenv subst n1 to_restrict
              in
                metasenv, subst