- lift added to CicMetaSubst

[helm.git] / helm / ocaml / cic_unification / cicMetaSubst.ml

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index a3b27c3e74548e86f2fd9dc712a979e3d9c23094..6d8b03ddb4c4d73832553ed172670b8ca2b00780 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -481,6 +481,16 @@ let unwind_subst metasenv subst =
 (* From now on we recreate a kernel abstraction where substitutions are part of
  * the calculus *)
 
+let lift metasenv subst n term =
+  (* TODO unwind's result is thrown away :-( *)
+  let (subst, _) = unwind_subst metasenv subst in
+  let term = apply_subst subst term in
+  try
+    CicSubstitution.lift n term
+  with e ->
+    raise (MetaSubstFailure ("Lift failure: " ^
+      Printexc.to_string e))
+
 let whd metasenv subst context term =
   (* TODO unwind's result is thrown away :-( *)
   let (subst, _) = unwind_subst metasenv subst in