Added new function compare_metasenvs.

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)
+;;

diff --git a/helm/ocaml/tactics/proofEngineHelpers.mli b/helm/ocaml/tactics/proofEngineHelpers.mli
index 5a4f145f995a07c1130f0b05460178fa2dd59f60..b0e3909409d0bf780dc77a5fda8ac408f87d44d1 100644 (file)
--- 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