From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 4 Feb 2004 14:33:04 +0000 (+0000)
Subject: Patch to delift withdrawn.
X-Git-Tag: V_0_2_3~69
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f49e4633ed1ee04f5492f03fbd3bac25046ecb0a;p=helm.git

Patch to delift withdrawn.
The patch was used to nullify items in the local context when they where
---

diff --git a/helm/ocaml/cic_unification/cicMetaSubst.ml b/helm/ocaml/cic_unification/cicMetaSubst.ml
index 04f32eb2c..da9cdb0ac 100644
--- 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 =