Patch to delift withdrawn.

[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 04f32eb2c77aaddf3ce18896f93cf6e9f95c497a..da9cdb0ac2e7902da622ec818c03f705747bc3d1 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -219,14 +219,6 @@ let rec restrict subst to_be_restricted metasenv =
 
 (*CSC: maybe we should rename delift in abstract, as I did in my dissertation *)
 let delift n subst context metasenv l t =
- let l =
-  let (_, canonical_context, _) = CicUtil.lookup_meta n metasenv in
-  List.map2 (fun ct lt ->
-    match (ct, lt) with
-    | None, _ -> None
-    | Some _, _ -> lt)
-    canonical_context l
- in
  let module S = CicSubstitution in
   let to_be_restricted = ref [] in
   let rec deliftaux k =