Added Instantiate ... in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7

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