From 46f7923521cdaea6117f02e5790806e9aa32ff9d Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Thu, 21 Sep 2006 13:24:39 +0000
Subject: [PATCH] apply now uses both menv and subst to decide the fresh meta
number
---
components/tactics/primitiveTactics.ml | 10 +++++-----
components/tactics/primitiveTactics.mli | 4 ++--
2 files changed, 7 insertions(+), 7 deletions(-)
diff --git a/components/tactics/primitiveTactics.ml b/components/tactics/primitiveTactics.ml
index 192460633..e09f0a1f7 100644
--- a/components/tactics/primitiveTactics.ml
+++ b/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/components/tactics/primitiveTactics.mli b/components/tactics/primitiveTactics.mli
index ce5194ad1..c30952cae 100644
--- a/components/tactics/primitiveTactics.mli
+++ b/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