X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Ftactics%2FproofEngineHelpers.ml;h=d78b94aface738467b4a0aa9ab906f525f619f6e;hb=275727242ccdce9df01af65f3bfb2d65283fa197;hp=03257dfa1bf46cdbd0563208d2170237e176fa1b;hpb=7ec7262cfa317c1962164350361f82a56c5d1826;p=helm.git

diff --git a/helm/ocaml/tactics/proofEngineHelpers.ml b/helm/ocaml/tactics/proofEngineHelpers.ml
index 03257dfa1..d78b94afa 100644
--- a/helm/ocaml/tactics/proofEngineHelpers.ml
+++ b/helm/ocaml/tactics/proofEngineHelpers.ml
@@ -28,8 +28,12 @@ let new_meta_of_proof ~proof:(_, metasenv, _, _) =
 
 let subst_meta_in_proof proof meta term newmetasenv =
  let uri,metasenv,bo,ty = proof in
-    (* empty context is ok for term since it wont be used by apply_subst *)
-  let subst_in = CicMetaSubst.apply_subst [meta,([], term)] in
+   (* empty context is ok for term since it wont be used by apply_subst *)
+   (* hack: since we do not know the context and the type of term, we
+      create a substitution with cc =[] and type = Implicit; they will be
+      in  any case dropped by apply_subst, but it would be better to rewrite
+      the code. Cannot we just use apply_subst_metasenv, etc. ?? *)
+  let subst_in = CicMetaSubst.apply_subst [meta,([], term,Cic.Implicit None)] in
    let metasenv' =
     newmetasenv @ (List.filter (function (m,_,_) -> m <> meta) metasenv)
    in