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 +++++++--
 proofs/evar_refiner.mli | 2 +-
 proofs/tacexpr.ml       | 2 +-
 3 files changed, 9 insertions(+), 4 deletions(-)

(limited to 'proofs')

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