]> matita.cs.unibo.it Git - helm.git/commitdiff
add comment
authorEnrico Tassi <enrico.tassi@inria.fr>
Fri, 17 Jul 2009 13:57:06 +0000 (13:57 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Fri, 17 Jul 2009 13:57:06 +0000 (13:57 +0000)
helm/software/components/grafite_engine/grafiteEngine.ml

index f1aea02da0a71efd0bece6fa26c0df667a5cc685..ceaa759622a741ab37768c6482fd415a0b62494e 100644 (file)
@@ -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