From 0d750a87e8b3f26964fc5a05cf559d86c913d962 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 18 Jun 2004 11:28:02 +0000 Subject: [PATCH] Added new function compare_metasenvs. --- helm/ocaml/tactics/proofEngineHelpers.ml | 6 ++++++ helm/ocaml/tactics/proofEngineHelpers.mli | 5 +++++ 2 files changed, 11 insertions(+) diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml index 2d576c3d8..73f465494 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.ml +++ b/helm/ocaml/tactics/proofEngineHelpers.ml @@ -96,3 +96,9 @@ let subst_meta_and_metasenv_in_proof proof meta subst_in newmetasenv = let newproof = uri,metasenv',bo',ty' in (newproof, metasenv') +let compare_metasenvs ~oldmetasenv ~newmetasenv = + List.map (function (i,_,_) -> i) + (List.filter + (function (i,_,_) -> + not (List.exists (fun (j,_,_) -> i=j) oldmetasenv)) newmetasenv) +;; diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli index 5a4f145f9..b0e390940 100644 --- a/helm/ocaml/tactics/proofEngineHelpers.mli +++ b/helm/ocaml/tactics/proofEngineHelpers.mli @@ -35,3 +35,8 @@ val subst_meta_and_metasenv_in_proof : ProofEngineTypes.proof -> int -> (Cic.term -> Cic.term) -> Cic.metasenv -> ProofEngineTypes.proof * Cic.metasenv + +(* returns the list of goals that are in newmetasenv and were not in + oldmetasenv *) +val compare_metasenvs : + oldmetasenv:Cic.metasenv -> newmetasenv:Cic.metasenv -> int list -- 2.39.2