more evar stuff

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

3 files changed, 9 insertions, 46 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 18bb5f24f1..b04691d87b 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -133,7 +133,7 @@ let w_Define sp c wc =
 
 (* w_tactic pour instantiate *) 
 
-let build_open_instance ev rawc wc =
+let w_refine ev rawc wc =
   if Evd.is_defined wc.sigma ev then 
     error "Instantiate called on already-defined evar";
   let e_info = Evd.map wc.sigma ev in
@@ -143,43 +143,9 @@ let build_open_instance ev rawc wc =
       (Some e_info.evar_concl) rawc in
     w_Define ev typed_c {wc with sigma=evd}
 
-(* The instantiate tactic *)
+(* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
 
-let evars_of evc c = 
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
-    | _ -> fold_constr evrec acc c
-  in 
-    evrec [] c
-
-let instantiate n rawc ido gl = 
-  let wc = Refiner.project_with_focus gl 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 ev,_ =  destEvar (List.nth evl (n-1)) in
-    let wc' = build_open_instance ev rawc wc in
-      tclIDTAC {it = gl.it ; sigma = wc'.sigma}
-
-let pfic gls c =
-  let evc = gls.sigma in 
-  Constrintern.interp_constr evc (Global.env_of_context gls.it.evar_hyps) c
-
-(*
-let instantiate_tac = function
-  | [Integer n; Command com] ->
-      (fun gl -> instantiate n (pfic gl com) gl)
-  | [Integer n; Constr c] ->
-      (fun gl -> instantiate n c gl)
-  | _ -> invalid_arg "Instantiate called with bad arguments"
-*)
-
-(* vernac command existential *)
+(* vernac command Existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
@@ -194,8 +160,6 @@ let instantiate_pf_com n com pfts =
   let e_info = Evd.map sigma sp in
   let env = Evarutil.evar_env e_info in
   let rawc = Constrintern.interp_rawconstr sigma env com in 
-  let wc' = build_open_instance sp rawc wc in
+  let wc' = w_refine sp rawc wc in
   let newgc = (w_Underlying wc') in
     change_constraints_pftreestate newgc pfts
-
-
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 55f5b96c22..2b5fbde423 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,9 +50,8 @@ 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 -> Rawterm.rawconstr -> 
-  identifier Tacexpr.gsimple_clause -> tactic
-(*
-val instantiate_tac : tactic_arg list -> tactic
-*)
+val w_refine :  evar -> Rawterm.rawconstr  -> w_tactic
+
 val instantiate_pf_com : int -> Topconstr.constr_expr -> pftreestate -> pftreestate
+
+(* the instantiate tactic was moved to tactics/evar_tactics.ml *) 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index b8c2636c06..e6e0c470ba 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -127,7 +127,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacGeneralize of 'constr list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause
-  | TacInstantiate of int * 'constr * 'id gclause
+  | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location)
 
   (* Derived basic tactics *)
   | TacSimpleInduction of (quantified_hypothesis * (bool ref * intro_pattern_expr list ref list) list ref)