From 55dd6231ab1fc6b8b1ffb900090681bcf0401e31 Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Mon, 19 Jun 2006 13:04:18 +0000 Subject: [PATCH] added (but still unused) remove_local_context --- .../components/tactics/paramodulation/equality.ml | 10 +++++++++- 1 file changed, 9 insertions(+), 1 deletion(-) 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 = -- 2.39.2