From b939b80860c675c83554d5d2e1a19ee9d233a34d Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Mon, 31 Jan 2005 17:10:38 +0000 Subject: [PATCH] Fixed bug in delift. The recursive call in the Meta case was on t and not on t lifted to the meta local context. --- helm/ocaml/cic_unification/cicMetaSubst.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 -- 2.39.2