diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/evar_refiner.ml | 9 | ||||
| -rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 2 |
3 files changed, 9 insertions, 4 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 3f3b66deee..0019b86010 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 c578ceeca4..a77b032233 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 062842e735..7ded6b4c92 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 |