diff options
Diffstat (limited to 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 9 |
1 files changed, 7 insertions, 2 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 |