From 6ce719daef6577d1a83c9e00a6ecc1dc42f17f7f Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 21 Sep 2006 13:24:39 +0000 Subject: [PATCH] apply now uses both menv and subst to decide the fresh meta number --- helm/software/components/tactics/primitiveTactics.ml | 10 +++++----- helm/software/components/tactics/primitiveTactics.mli | 4 ++-- 2 files changed, 7 insertions(+), 7 deletions(-) diff --git a/helm/software/components/tactics/primitiveTactics.ml b/helm/software/components/tactics/primitiveTactics.ml index 192460633..e09f0a1f7 100644 --- a/helm/software/components/tactics/primitiveTactics.ml +++ b/helm/software/components/tactics/primitiveTactics.ml @@ -246,14 +246,14 @@ let rec count_prods context ty = Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t | _ -> 0 -let apply_tac_verbose_with_subst ~term (proof, goal) = +let apply_with_subst ~term ~subst (proof, goal) = (* Assumption: The term "term" must be closed in the current context *) let module T = CicTypeChecker in let module R = CicReduction in let module C = Cic in let (_,metasenv,_,_) = proof in let metano,context,ty = CicUtil.lookup_meta goal metasenv in - let newmeta = new_meta_of_proof ~proof in + let newmeta = CicMkImplicit.new_meta metasenv subst in let exp_named_subst_diff,newmeta',newmetasenvfragment,term' = match term with C.Var (uri,exp_named_subst) -> @@ -326,10 +326,10 @@ let apply_tac_verbose_with_subst ~term (proof, goal) = (* ALB *) -let apply_tac_verbose_with_subst ~term status = +let apply_with_subst ~term ?(subst=[]) status = try (* apply_tac_verbose ~term status *) - apply_tac_verbose_with_subst ~term status + apply_with_subst ~term ~subst status (* TODO cacciare anche altre eccezioni? *) with | CicUnification.UnificationFailure msg @@ -338,7 +338,7 @@ let apply_tac_verbose_with_subst ~term status = (* ALB *) let apply_tac_verbose ~term status = - let subst, status = apply_tac_verbose_with_subst ~term status in + let subst, status = apply_with_subst ~term status in (CicMetaSubst.apply_subst subst), status let apply_tac ~term status = snd (apply_tac_verbose ~term status) diff --git a/helm/software/components/tactics/primitiveTactics.mli b/helm/software/components/tactics/primitiveTactics.mli index ce5194ad1..c30952cae 100644 --- a/helm/software/components/tactics/primitiveTactics.mli +++ b/helm/software/components/tactics/primitiveTactics.mli @@ -43,8 +43,8 @@ val classify_metas : (Cic.term * Cic.context * Cic.term) list (* ALB, needed by the new paramodulation... *) -val apply_tac_verbose_with_subst: - term:Cic.term -> ProofEngineTypes.proof * int -> +val apply_with_subst: + term:Cic.term -> ?subst:Cic.substitution -> ProofEngineTypes.proof * int -> Cic.substitution * (ProofEngineTypes.proof * int list) (* not a real tactic *) -- 2.39.2