add comment

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index f1aea02da0a71efd0bece6fa26c0df667a5cc685..ceaa759622a741ab37768c6482fd415a0b62494e 100644 (file)
--- 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