From a008023cae4fdddffbbbfd8a455d7776200a9cfb Mon Sep 17 00:00:00 2001
From: corbinea
Date: Thu, 6 Nov 2003 14:35:25 +0000
Subject: Added Instantiate ... in

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4820 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/evar_refiner.ml | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

(limited to 'proofs/evar_refiner.ml')

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 
-- 
cgit v1.2.3