Fixing bug #2308 ("instantiate" tactic did not comply with

the interpretation mechanism of ltac variables)



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

3 files changed, 13 insertions, 15 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8b7a7d99f..e2bce9fde 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -25,7 +25,6 @@ open Logic
 open Reduction
 open Reductionops
 open Tacmach
-open Evar_refiner
 open Rawterm
 open Pattern
 open Tacexpr
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index e1236bbaa..d7a1232ad 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -20,23 +20,20 @@ open Refiner
 (* Instantiation of existential variables *)
 (******************************************)
 
-(* w_tactic pour instantiate *) 
-
-let w_refine evk rawc evd =
-  if Evd.is_defined ( evd) evk then 
+let w_refine (evk,evi) (ltac_var,rawc) sigma =
+  if Evd.is_defined sigma evk then
     error "Instantiate called on already-defined evar";
-  let e_info = Evd.find ( evd) evk in
-  let env = Evd.evar_env e_info in
-  let sigma,typed_c =
-    try Pretyping.Default.understand_tcc ~resolve_classes:false
-      ( evd) env ~expected_type:e_info.evar_concl rawc
+  let env = Evd.evar_env evi in
+  let sigma',typed_c =
+    try Pretyping.Default.understand_ltac sigma env ltac_var
+	  (Pretyping.OfType (Some evi.evar_concl)) rawc
     with _ ->
       let loc = Rawterm.loc_of_rawconstr rawc in
       user_err_loc 
         (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
 			string_of_existential evk))
   in
-    define evk typed_c (evars_reset_evd sigma evd)
+    define evk typed_c (evars_reset_evd sigma' sigma)
 
 (* vernac command Existential *)
 
@@ -54,6 +51,5 @@ let instantiate_pf_com n com pfts =
   in 
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
-  let evd = create_goal_evar_defs sigma in
-  let evd' = w_refine evk rawc evd in
-    change_constraints_pftreestate ( evd') pfts
+  let sigma' = w_refine (evk,evi) (([],[]),rawc) sigma in
+  change_constraints_pftreestate sigma' pfts
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 7b9da802c..a35a9b58b 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -14,11 +14,14 @@ open Term
 open Environ
 open Evd
 open Refiner
+open Pretyping
+open Rawterm
 (*i*)
 
 (* Refinement of existential variables. *)
 
-val w_refine : evar -> Rawterm.rawconstr  -> evar_defs -> evar_defs
+val w_refine : evar * evar_info -> 
+  (var_map * unbound_ltac_var_map) * rawconstr -> evar_defs -> evar_defs
 
 val instantiate_pf_com :
   int -> Topconstr.constr_expr -> pftreestate -> pftreestate