From: Andrea Asperti <andrea.asperti@unibo.it>
Date: Fri, 27 Apr 2007 13:46:36 +0000 (+0000)
Subject: Apply_with_subst now returns a subst with a correct type for the meta.
X-Git-Tag: make_still_working~6357
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=025d672d177e34a01c59f188fcf7a13e93bb89c8;p=helm.git

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 cc16c2030..5c7af528f 100644
--- 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)