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 1e9e97ec58f3147733356cfde501a72bdf83da74..10c0aa8d4c8dba048ffab45914698a775303d1c7 100644 (file)
--- 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 =