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 /proofs | |
| 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 '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 |