diff options
| author | corbinea | 2003-11-06 14:35:25 +0000 |
|---|---|---|
| committer | corbinea | 2003-11-06 14:35:25 +0000 |
| commit | a008023cae4fdddffbbbfd8a455d7776200a9cfb (patch) | |
| tree | c2b82f43339ee45d614395d7350d6b53a8364437 /tactics | |
| parent | b74a68a56164f952345ba083f42b95eaaa37355e (diff) | |
Added Instantiate ... in
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 4 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 9 |
3 files changed, 9 insertions, 6 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 046ae4ed1e..5dc25889b6 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -46,8 +46,8 @@ let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c) let h_let_tac id c cl = abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl) -let h_instantiate n c = - abstract_tactic (TacInstantiate (n,c)) (Evar_refiner.instantiate n c) +let h_instantiate n c ido = + abstract_tactic (TacInstantiate (n,c,ido)) (Evar_refiner.instantiate n c ido) (* Derived basic tactics *) let h_simple_induction h = diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 82146c01aa..26e05eb31d 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -49,7 +49,7 @@ val h_generalize : constr list -> tactic val h_generalize_dep : constr -> tactic val h_forward : bool -> name -> constr -> tactic val h_let_tac : identifier -> constr -> identifier clause_pattern -> tactic -val h_instantiate : int -> constr -> tactic +val h_instantiate : int -> constr -> Tacticals.clause -> tactic (* Derived basic tactics *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 77518de856..fad326f1ab 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -594,7 +594,9 @@ let rec intern_atomic lf ist x = | TacLetTac (id,c,clp) -> let id = intern_ident lf ist id in TacLetTac (id,intern_constr ist c,intern_clause_pattern ist clp) - | TacInstantiate (n,c) -> TacInstantiate (n,intern_constr ist c) + | TacInstantiate (n,c,ido) -> + TacInstantiate (n,intern_constr ist c, + (option_app (intern_hyp_or_metaid ist) ido)) (* Automation tactics *) | TacTrivial l -> TacTrivial l @@ -1593,7 +1595,8 @@ and interp_atomic ist gl = function | TacLetTac (id,c,clp) -> let clp = interp_clause_pattern ist gl clp in h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp - | TacInstantiate (n,c) -> h_instantiate n (pf_interp_constr ist gl c) + | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c) + (option_app (interp_hyp ist gl) ido) (* Automation tactics *) | TacTrivial l -> Auto.h_trivial l @@ -1838,7 +1841,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl) | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c) | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp) - | TacInstantiate (n,c) -> TacInstantiate (n,subst_rawconstr subst c) + | TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido) (* Automation tactics *) | TacTrivial l -> TacTrivial l |