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 ae5299dc588a11bd8fb59ef660fff725ebe0c5fb..d18458e2bb711f486e9f5fe557c6390cffb48c3c 100644 (file)
--- 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