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 a28b853bebabcfe3eb9be907cedd24bda2bff868..da9cdb0ac2e7902da622ec818c03f705747bc3d1 100644 (file)
--- a/helm/ocaml/cic_unification/cicMetaSubst.ml
+++ b/helm/ocaml/cic_unification/cicMetaSubst.ml
@@ -205,7 +205,7 @@ let rec restrict subst to_be_restricted metasenv =
                 "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since ?%d is already instantiated with %s and at least one of the hypotheses occurs in the substituted term"
                 n (names_of_context_indexes context to_be_restricted) n
                 (CicPp.ppterm s)))
-          with Not_found -> (more @ more_to_be_restricted, metasenv', subst))
+           with Not_found -> (more @ more_to_be_restricted @ more_to_be_restricted', metasenv', subst))
         with Occur ->
           raise (MetaSubstFailure (sprintf
             "Cannot restrict the context of the metavariable ?%d over the hypotheses %s since metavariable's type depends on at least one of them"
@@ -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 =
@@ -475,6 +467,14 @@ let rec apply_subst_context subst context =
       | None -> None :: context)
     context []
 
+let apply_subst_metasenv subst metasenv =
+  List.map
+    (fun (n, context, ty) ->
+      (n, apply_subst_context subst context, apply_subst subst ty))
+    (List.filter
+      (fun (i, _, _) -> not (List.exists (fun (j, _) -> (j = i)) subst))
+      metasenv)
+
 let ppterm subst term = CicPp.ppterm (apply_subst subst term)
 
 let ppcontext ?(sep = "\n") subst context =