From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 31 Jan 2005 17:10:38 +0000 (+0000)
Subject: Fixed bug in delift. The recursive call in the Meta case was on t and not
X-Git-Tag: V_0_1_0~88
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b939b80860c675c83554d5d2e1a19ee9d233a34d;p=helm.git

Fixed bug in delift. The recursive call in the Meta case was on t and not
on t lifted to the meta local context.
---

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