effective evar refining

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

5 files changed, 34 insertions, 16 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 2273ee760f..18bb5f24f1 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -11,7 +11,9 @@
 open Pp
 open Util
 open Names
+open Rawterm
 open Term
+open Termops
 open Environ
 open Evd
 open Sign
@@ -129,6 +131,18 @@ let w_Define sp c wc =
 (* Instantiation of existential variables *)
 (******************************************)
 
+(* w_tactic pour instantiate *) 
+
+let build_open_instance 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
+  let env = Evarutil.evar_env e_info in
+  let evd,typed_c = 
+    Pretyping.understand_gen_tcc wc.sigma env [] 
+      (Some e_info.evar_concl) rawc in
+    w_Define ev typed_c {wc with sigma=evd}
+
 (* The instantiate tactic *)
 
 let evars_of evc c = 
@@ -137,9 +151,9 @@ let evars_of evc c =
     | Evar (n, _) when Evd.in_dom evc n -> c :: acc
     | _ -> fold_constr evrec acc c
   in 
-  evrec [] c
+    evrec [] c
 
-let instantiate n c ido gl = 
+let instantiate n rawc ido gl = 
   let wc = Refiner.project_with_focus gl in
   let evl = 
     match ido with
@@ -148,11 +162,9 @@ let instantiate n c ido gl =
 	  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 
-	error "Instantiate called on already-defined evar";
-      let wc' = w_Define n c wc in 
-	tclIDTAC {it = gl.it ; sigma = wc'.sigma}
+    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 
@@ -173,15 +185,17 @@ let instantiate_pf_com n com pfts =
   let gls = top_goal_of_pftreestate pfts in
   let wc = project_with_focus gls in
   let sigma = (w_Underlying wc) in 
-  let (sp,evd) = 
+  let (sp,evd) (* as evc *) = 
     try
       List.nth (Evd.non_instantiated sigma) (n-1) 
     with Failure _ -> 
       error "not so many uninstantiated existential variables"
   in 
-  let c = Constrintern.interp_constr sigma (Evarutil.evar_env evd) com in     
-  let wc' = w_Define sp c wc in
+  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 newgc = (w_Underlying wc') in
-  change_constraints_pftreestate newgc pfts
+    change_constraints_pftreestate newgc pfts
 
 
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index d5f11b6d4b..55f5b96c22 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -50,7 +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 -> constr -> identifier Tacexpr.gsimple_clause -> tactic
+val instantiate : int -> Rawterm.rawconstr -> 
+  identifier Tacexpr.gsimple_clause -> tactic
 (*
 val instantiate_tac : tactic_arg list -> tactic
 *)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 99fe569bb7..21f7d43fc7 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -48,8 +48,9 @@ let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c)
 let h_let_tac na c cl =
   abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl)
 let h_instantiate n c cls = 
-  abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (simple_clause_of cls))
+(Evar_refiner.instantiate n c (simple_clause_of cls))
+  (* abstract_tactic (TacInstantiate (n,c,cls))
+    (Evar_refiner.instantiate n c (simple_clause_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 7c8c1b3c56..90a2d1b3c3 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -50,7 +50,8 @@ val h_generalize      : constr list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_forward         : bool -> name -> constr -> tactic 
 val h_let_tac         : name -> constr -> Tacticals.clause -> tactic
-val h_instantiate     : int -> constr -> Tacticals.clause -> tactic
+val h_instantiate     : int -> Rawterm.rawconstr -> 
+  Tacticals.clause -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 06a4c90a75..fe557c9fcf 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1712,7 +1712,8 @@ and interp_atomic ist gl = function
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
       h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp
-  | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c)
+  | TacInstantiate (n,c,ido) -> h_instantiate n (fst c) 
+      (* pf_interp_constr ist gl c *)
       (clause_app (interp_hyp_location ist gl) ido)
 
   (* Automation tactics *)