X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=03257dfa1bf46cdbd0563208d2170237e176fa1b;hb=a864255e782859e2b3b7da08297f5d3fe2ee710d;hp=73f465494898b99d1ca24efc0db5f7f6a12d1300;hpb=0d750a87e8b3f26964fc5a05cf559d86c913d962;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 73f465494..03257dfa1 100644
--- 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