New handling of substitution:

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

diff --git a/helm/ocaml/tactics/primitiveTactics.ml b/helm/ocaml/tactics/primitiveTactics.ml
index 2d741f1d1c317a72cfcf62d9b25be6f4cf88f496..cc743d7cc66e90e9a43651f9ea539c0c71b638e9 100644 (file)
--- a/helm/ocaml/tactics/primitiveTactics.ml
+++ b/helm/ocaml/tactics/primitiveTactics.ml
@@ -326,7 +326,9 @@ let apply_tac ~term (proof, goal) =
          in
           let newmetasenv'' = new_uninstantiatedmetas@old_uninstantiatedmetas in
           let (newproof, newmetasenv''') =
-           let subst_in = CicMetaSubst.apply_subst ((metano,bo')::subst) in
+           let subst_in =
+             CicMetaSubst.apply_subst ((metano,(context, bo'))::subst)
+           in
             subst_meta_and_metasenv_in_proof
               proof metano subst_in newmetasenv''
           in
@@ -501,7 +503,7 @@ let elim_tac ~term =
            C.Appl (eliminator_ref :: make_tl term (args_no - 1))
          in
           let metasenv', term_to_refine' =
-           CicMkImplicit.expand_implicits metasenv context term_to_refine in
+           CicMkImplicit.expand_implicits metasenv [] context term_to_refine in
           let refined_term,_,metasenv'' =
            CicRefine.type_of_aux' metasenv' context term_to_refine'
           in