X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_unification%2FcicMetaSubst.ml;h=d18458e2bb711f486e9f5fe557c6390cffb48c3c;hb=4cb4d286a1fdcb150c2848a9d21ac3486906c317;hp=ae5299dc588a11bd8fb59ef660fff725ebe0c5fb;hpb=9369ab9136d5726669b30f3598f2e433fba438d9;p=helm.git

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index ae5299dc5..d18458e2b 100644
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -657,7 +657,7 @@ let delift n subst context metasenv l t =
      | C.Meta (i, l1) as t -> 
          (try
            let (_,t,_) = CicUtil.lookup_subst i subst in
-           deliftaux k t
+             deliftaux k (CicSubstitution.lift_meta l1 t)
          with CicUtil.Subst_not_found _ ->
            (* see the top level invariant *)
            if (i = n) then