From: Andrea Asperti Date: Mon, 19 Jun 2006 13:04:18 +0000 (+0000) Subject: added (but still unused) remove_local_context X-Git-Tag: 0.4.95@7852~1296 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b0e4928e8b7eeab413c44ffdcc8b9c5bd90dbf4c;p=helm.git added (but still unused) remove_local_context --- diff --git a/components/tactics/paramodulation/equality.ml b/components/tactics/paramodulation/equality.ml index 1e9e97ec5..10c0aa8d4 100644 --- a/components/tactics/paramodulation/equality.ml +++ b/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 =