debian version 0.6.3-2

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

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 2d576c3d8badf7c3f760041e3aa40d2a808e563b..03257dfa1bf46cdbd0563208d2170237e176fa1b 100644 (file)
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -24,11 +24,12 @@
  *)
 
 let new_meta_of_proof ~proof:(_, metasenv, _, _) =
-  CicMkImplicit.new_meta metasenv
+  CicMkImplicit.new_meta metasenv []
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,bo,ty = proof in
-  let subst_in = CicMetaSubst.apply_subst [meta,term] in
+    (* empty context is ok for term since it wont be used by apply_subst *)
+  let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
    in
@@ -96,3 +97,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)
+;;