From b964a69273d19ed84a7a3d089fceaf475f8ae1ea Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Fri, 17 Jul 2009 13:57:06 +0000 Subject: [PATCH] add comment --- helm/software/components/grafite_engine/grafiteEngine.ml | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml index f1aea02da..ceaa75962 100644 --- a/helm/software/components/grafite_engine/grafiteEngine.ml +++ b/helm/software/components/grafite_engine/grafiteEngine.ml @@ -565,7 +565,12 @@ let close_in_context t metasenv = (i,(tag,[],NCic.Rel (m-List.length ctx),ty))::(m_subst m) in NCic.Lambda (name, ty, aux m_subst subst ((name,NCic.Decl ty)::ctx) tl) - | [] -> NCicUntrusted.apply_subst subst ctx + | [] -> + (* STRONG ASSUMPTION: + since metas occurring in t have an empty context, + the substitution i build makes sense (i.e, the Rel + I pun in the subst will not be lifted by subst_meta *) + NCicUntrusted.apply_subst subst ctx (NCicSubstitution.lift (List.length ctx) t) | _ -> assert false in -- 2.39.2