From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Mon, 19 Jun 2006 13:04:18 +0000 (+0000)
Subject: added (but still unused) remove_local_context
X-Git-Tag: make_still_working~7162
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=55dd6231ab1fc6b8b1ffb900090681bcf0401e31;p=helm.git

added (but still unused) remove_local_context
---

diff --git a/helm/software/components/tactics/paramodulation/equality.ml b/helm/software/components/tactics/paramodulation/equality.ml
index 1e9e97ec5..10c0aa8d4 100644
--- a/helm/software/components/tactics/paramodulation/equality.ml
+++ b/helm/software/components/tactics/paramodulation/equality.ml
@@ -747,6 +747,15 @@ let metas_of_proof p =
   Utils.metas_of_term p
 ;;
 
+let remove_local_context eq =
+   let w, p, (ty, left, right, o), menv,id = open_equality eq in
+   let p = Utils.remove_local_context p in
+   let ty = Utils.remove_local_context ty in
+   let left = Utils.remove_local_context left in
+   let right = Utils.remove_local_context right in
+   w, p, (ty, left, right, o), menv, id
+;;
+
 let relocate newmeta menv to_be_relocated =
   let subst, newmetasenv, newmeta = 
     List.fold_right 
@@ -761,7 +770,6 @@ let relocate newmeta menv to_be_relocated =
   let menv = Subst.apply_subst_metasenv subst menv @ newmetasenv in
   subst, menv, newmeta
 
-
 let fix_metas newmeta eq = 
   let w, p, (ty, left, right, o), menv,_ = open_equality eq in
   let to_be_relocated =