From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 17 Jul 2009 13:57:06 +0000 (+0000)
Subject: add comment
X-Git-Tag: make_still_working~3666
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b964a69273d19ed84a7a3d089fceaf475f8ae1ea;p=helm.git

add comment
---

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