Apply_with_subst now returns a subst with a correct type for the meta.

diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml
index cc16c203012101be0aff7f3657da38dded372b8d..5c7af528f04df92dd4f3df1e8069a72969d5fbf6 100644 (file)
--- a/helm/software/components/tactics/primitiveTactics.ml
+++ b/helm/software/components/tactics/primitiveTactics.ml
@@ -234,12 +234,13 @@ let
     new_fresh_meta,newmetasenvfragment,exp_named_subst',exp_named_subst_diff
 ;;
 
-let new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty termty goal_arity =
+let new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty termty goal_arity =
   let (consthead,newmetasenv,arguments,_) =
    TermUtil.saturate_term newmeta' metasenv' context termty
     goal_arity in
   let subst,newmetasenv',_ = 
-   CicUnification.fo_unif newmetasenv context consthead ty CicUniv.empty_ugraph
+   CicUnification.fo_unif_subst 
+     subst context newmetasenv consthead ty CicUniv.empty_ugraph
   in
   let t = 
     if List.length arguments = 0 then term' else Cic.Appl (term'::arguments)
@@ -301,7 +302,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
    let subst,newmetasenv',t = 
     let rec add_one_argument n =
      try
-      new_metasenv_and_unify_and_t newmeta' metasenv' context term' ty
+      new_metasenv_and_unify_and_t newmeta' metasenv' subst context term' ty
         termty n
      with CicUnification.UnificationFailure _ when n > 0 ->
       add_one_argument (n - 1)
@@ -326,7 +327,7 @@ let apply_with_subst ~term ~subst ~maxmeta (proof, goal) =
     ProofEngineHelpers.subst_meta_and_metasenv_in_proof proof metano subst_in
      newmetasenv''
    in
-   let subst = ((metano,(context,bo',Cic.Implicit None))::subst) in
+   let subst = ((metano,(context,bo',ty))::subst) in
    subst,
    (newproof, List.map (function (i,_,_) -> i) new_uninstantiatedmetas),
    max maxmeta (CicMkImplicit.new_meta newmetasenv''' subst)