From: Andrea Asperti 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)