aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--contrib/interface/xlate.ml5
-rw-r--r--parsing/g_tactic.ml45
-rw-r--r--parsing/g_tacticnew.ml47
-rw-r--r--parsing/pptactic.ml6
-rw-r--r--proofs/evar_refiner.ml9
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/tacexpr.ml2
-rw-r--r--tactics/hiddentac.ml4
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/tacinterp.ml9
-rw-r--r--translate/pptacticnew.ml10
11 files changed, 40 insertions, 21 deletions
diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 58eaf292a..47370ef13 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1010,8 +1010,11 @@ and xlate_tac =
(xlate_int_or_constr a, xlate_using b,
CT_id_list_list
(List.map (fun l -> CT_id_list(List.map xlate_newind_names l)) c))
- | TacInstantiate (a, b) ->
+ | TacInstantiate (a, b, None) ->
CT_instantiate(CT_int a, xlate_formula b)
+ | TacInstantiate (a, b, _) ->
+ xlate_error "TODO: Instantiate ... in"
+
| TacLetTac (id, c, cl) ->
CT_lettac(xlate_ident id, xlate_formula c,
(* TODO LATER: This should be shared with Unfold,
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 47977b69b..74352c0bb 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -292,8 +292,9 @@ GEXTEND Gram
| IDENT "Generalize"; IDENT "Dependent"; c = constr -> TacGeneralizeDep c
| IDENT "LetTac"; id = base_ident; ":="; c = constr; p = clause_pattern
-> TacLetTac (id,c,p)
- | IDENT "Instantiate"; n = natural; c = constr -> TacInstantiate (n,c)
-
+ | IDENT "Instantiate"; n = natural; c = constr;
+ ido = OPT [ "in"; id = id_or_ltac_ref -> id ] ->
+ TacInstantiate (n,c,ido)
| IDENT "Specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
| IDENT "LApply"; c = constr -> TacLApply c
diff --git a/parsing/g_tacticnew.ml4 b/parsing/g_tacticnew.ml4
index 59dd34769..d98f8ad45 100644
--- a/parsing/g_tacticnew.ml4
+++ b/parsing/g_tacticnew.ml4
@@ -344,9 +344,10 @@ GEXTEND Gram
TacGeneralizeDep c
| IDENT "set"; "("; id = base_ident; ":="; c = lconstr; ")";
p = clause_pattern -> TacLetTac (id,c,p)
- | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" ->
- TacInstantiate (n,c)
-
+ | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")";
+ ido = OPT [ "in"; id = id_or_meta -> id ] ->
+ TacInstantiate (n,c,ido)
+
| IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings ->
TacSpecialize (n,lcb)
| IDENT "lapply"; c = constr -> TacLApply c
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 9e1e3498f..8f0a29c64 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -454,9 +454,11 @@ and pr_atom1 = function
| TacLetTac (id,c,cl) ->
hov 1 (str "LetTac" ++ spc () ++ pr_id id ++ str ":=" ++
pr_constr c ++ pr_clause_pattern pr_ident cl)
- | TacInstantiate (n,c) ->
+ | TacInstantiate (n,c,None) ->
hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c)
-
+ | TacInstantiate (n,c,Some id) ->
+ hov 1 (str "Instantiate" ++ pr_arg int n ++ pr_arg pr_constr c ++
+ spc () ++ str "in" ++ pr_arg pr_ident id)
(* Derived basic tactics *)
| TacSimpleInduction h ->
hov 1 (str "Induction" ++ pr_arg pr_quantified_hypothesis h)
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 3f3b66dee..0019b8601 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -133,9 +133,14 @@ let evars_of evc c =
in
evrec [] c
-let instantiate n c gl =
+let instantiate n c ido gl =
let wc = Refiner.project_with_focus gl in
- let evl = evars_of wc.sigma gl.it.evar_concl in
+ let evl =
+ match ido with
+ None -> evars_of wc.sigma gl.it.evar_concl
+ | Some id ->
+ let (_,_,typ)=Sign.lookup_named id gl.it.evar_hyps in
+ evars_of wc.sigma typ in
if List.length evl < n then error "not enough evars";
let (n,_) as k = destEvar (List.nth evl (n-1)) in
if Evd.is_defined wc.sigma n then
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index c578ceeca..a77b03223 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +50,7 @@ val w_conv_x : wc -> constr -> constr -> bool
val w_const_value : wc -> constant -> constr
val w_defined_evar : wc -> existential_key -> bool
-val instantiate : int -> constr -> tactic
+val instantiate : int -> constr -> Tacticals.clause -> tactic
(*
val instantiate_tac : tactic_arg list -> tactic
*)
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 062842e73..7ded6b4c9 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -118,7 +118,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
| TacGeneralize of 'constr list
| TacGeneralizeDep of 'constr
| TacLetTac of identifier * 'constr * 'id clause_pattern
- | TacInstantiate of int * 'constr
+ | TacInstantiate of int * 'constr * 'id option
(* Derived basic tactics *)
| TacSimpleInduction of quantified_hypothesis
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 046ae4ed1..5dc25889b 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 82146c01a..26e05eb31 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 77518de85..fad326f1a 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
diff --git a/translate/pptacticnew.ml b/translate/pptacticnew.ml
index 0dbc08250..035cdfd63 100644
--- a/translate/pptacticnew.ml
+++ b/translate/pptacticnew.ml
@@ -455,11 +455,15 @@ and pr_atom1 env = function
hov 1 (str"(" ++ pr_id id ++ str " :=" ++
pr_lconstrarg env c ++ str")") ++
pr_clause_pattern pr_ident cl)
- | TacInstantiate (n,c) ->
+ | TacInstantiate (n,c,None) ->
hov 1 (str "instantiate" ++ spc() ++
hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
- pr_lconstrarg env c ++ str")"))
-
+ pr_lconstrarg env c ++ str ")"))
+ | TacInstantiate (n,c,Some id) ->
+ hov 1 (str "instantiate" ++ spc() ++
+ hov 1 (str"(" ++ pr_arg int n ++ str" :=" ++
+ pr_lconstrarg env c ++ str ")" ++
+ spc () ++ str "in" ++ pr_arg pr_ident id))
(* Derived basic tactics *)
| TacSimpleInduction h ->
hov 1 (str "simple_induction" ++ pr_arg pr_quantified_hypothesis h)
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 22:17:13 +0000