Added new function compare_metasenvs.

[helm.git] / helm / ocaml / tactics / proofEngineHelpers.ml

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 2d576c3d8badf7c3f760041e3aa40d2a808e563b..73f465494898b99d1ca24efc0db5f7f6a12d1300 100644 (file)
--- 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)
+;;