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

13 files changed, 40 insertions, 50 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 8b7a7d99f6..e2bce9fde1 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 e1236bbaa8..d7a1232ad0 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 7b9da802c1..a35a9b58b0 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
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index d03b26192c..0d08b72aae 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -29,7 +29,7 @@ let evar_list evc c =
   in 
     evrec [] c
 
-let instantiate n rawc ido gl = 
+let instantiate n (ist,rawc) ido gl = 
   let sigma = gl.sigma in
   let evl = 
     match ido with
@@ -49,31 +49,19 @@ let instantiate n rawc ido gl =
 		      (_,Some body,_) -> evar_list sigma body
 		    | _ -> error "Not a defined hypothesis.") in
     if List.length evl < n then
-      error "not enough uninstantiated existential variables";
+      error "Not enough uninstantiated existential variables.";
     if n <= 0 then error "Incorrect existential variable index.";
-    let ev,_ =  destEvar (List.nth evl (n-1)) in
-    let evd' = w_refine ev rawc (create_goal_evar_defs sigma) in
+    let evk,_ = destEvar (List.nth evl (n-1)) in
+    let evi = Evd.find sigma evk in
+    let ltac_vars = Tacinterp.extract_ltac_vars ist sigma (Evd.evar_env evi) in
+    let sigma' = w_refine (evk,evi) (ltac_vars,rawc) sigma in
       tclTHEN
-        (tclEVARS ( evd'))
+        (tclEVARS sigma')
         tclNORMEVAR
         gl
 	
-(*
-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"
-*)
-
 let let_evar name typ gls =
-  let evd = Evd.create_goal_evar_defs gls.sigma in
-  let evd',evar = Evarutil.new_evar evd (pf_env gls) typ in
-  Refiner.tclTHEN (Refiner.tclEVARS ( evd'))
+  let sigma',evar = Evarutil.new_evar gls.sigma (pf_env gls) typ in
+  Refiner.tclTHEN (Refiner.tclEVARS sigma')
     (Tactics.letin_tac None name evar None nowhere) gls
  
diff --git a/tactics/evar_tactics.mli b/tactics/evar_tactics.mli
index 66b24153ad..7a305f2001 100644
--- a/tactics/evar_tactics.mli
+++ b/tactics/evar_tactics.mli
@@ -13,7 +13,7 @@ open Names
 open Tacexpr
 open Termops
 
-val instantiate : int -> Rawterm.rawconstr -> 
+val instantiate : int -> Tacinterp.interp_sign * Rawterm.rawconstr -> 
   (identifier * hyp_location_flag, unit) location -> tactic
 
 (*i
diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 0eb4a76f3a..4e3e04c67f 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -100,9 +100,9 @@ END
 
 let pr_gen prc _prlc _prtac c = prc c
 
-let pr_rawc _prc _prlc _prtac raw = Printer.pr_rawconstr raw
+let pr_rawc _prc _prlc _prtac (_,raw) = Printer.pr_rawconstr raw
 
-let interp_raw _ _ (t,_) = t
+let interp_raw ist gl (t,_) = (ist,t)
 
 let glob_raw = Tacinterp.intern_constr
 
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index b27d8fffc8..4492fd8421 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -25,7 +25,7 @@ val rawwit_occurrences : (int list or_var) raw_abstract_argument_type
 val wit_occurrences : (int list) typed_abstract_argument_type
 
 val rawwit_raw : constr_expr raw_abstract_argument_type
-val wit_raw : rawconstr typed_abstract_argument_type
+val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type
 val raw : constr_expr Pcoq.Gram.Entry.e
 
 type 'id gen_place= ('id * hyp_location_flag,unit) location
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 60916fda4c..2aff94b640 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -75,10 +75,6 @@ let h_generalize_dep c =
 let h_let_tac b na c cl =
   let with_eq = if b then None else Some (true,(dummy_loc,IntroAnonymous)) in
   abstract_tactic (TacLetTac (na,inj_open c,cl,b)) (letin_tac with_eq na c None cl)
-let h_instantiate n c ido = 
-(Evar_tactics.instantiate n c ido)
-  (* abstract_tactic (TacInstantiate (n,c,cls))
-    (Evar_refiner.instantiate n c (goal_location_of cls)) *)
 
 (* Derived basic tactics *)
 let h_simple_induction_destruct isrec h =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index faa8c4150d..5aafb91a0d 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -62,8 +62,6 @@ val h_generalize_gen  : (constr with_occurrences * name) list -> tactic
 val h_generalize_dep  : constr -> tactic 
 val h_let_tac         : letin_flag -> name -> constr -> 
                         Tacticals.clause -> tactic
-val h_instantiate     : int -> Rawterm.rawconstr ->
-  (identifier * hyp_location_flag, unit) location -> tactic
 
 (* Derived basic tactics *)
 
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index a7b3a15e3a..da7ae038ab 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1401,6 +1401,14 @@ let retype_list sigma env lst =
     try (x,Retyping.get_judgment_of env sigma csr)::a with
     | Anomaly _ -> a) lst []
 
+let extract_ltac_vars_data ist sigma env =
+  let (ltacvars,_ as vars) = constr_list ist env in
+  vars, retype_list sigma env ltacvars
+
+let extract_ltac_vars ist sigma env =
+  let (_,unbndltacvars),typs = extract_ltac_vars_data ist sigma env in
+  typs,unbndltacvars
+
 let implicit_tactic = ref None
 
 let declare_implicit_tactic tac = implicit_tactic := Some tac
@@ -1446,8 +1454,8 @@ let solve_remaining_evars env initial_sigma evd c =
   proc_rec (Evarutil.nf_isevar !evdref c)
 
 let interp_gen kind ist sigma env (c,ce) =
-  let (ltacvars,unbndltacvars as vars) = constr_list ist env in
-  let typs = retype_list sigma env ltacvars in
+  let (ltacvars,unbndltacvars as vars),typs =
+    extract_ltac_vars_data ist sigma env in
   let c = match ce with
   | None -> c
     (* If at toplevel (ce<>None), the error can be due to an incorrect
diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli
index 6faae3adc1..6b7aabe2e3 100644
--- a/tactics/tacinterp.mli
+++ b/tactics/tacinterp.mli
@@ -44,6 +44,9 @@ and interp_sign =
     debug : debug_info;
     trace : ltac_trace }
 
+val extract_ltac_vars : interp_sign -> Evd.evar_defs -> Environ.env -> 
+  Pretyping.var_map * Pretyping.unbound_ltac_var_map
+
 (* Transforms an id into a constr if possible *)
 val constr_of_id : Environ.env -> identifier -> constr
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index fa23cfb857..ab7120b8be 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -26,7 +26,6 @@ open Clenvtac
 open Rawterm
 open Pattern
 open Matching
-open Evar_refiner
 open Genarg
 open Tacexpr
 
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index 220c8e782d..0a0cfb79b4 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -5,7 +5,6 @@ Nbtermdn
 Tacticals
 Hipattern
 Tactics
-Evar_tactics
 Hiddentac
 Elim
 Dhyp
@@ -16,6 +15,7 @@ Contradiction
 Inv
 Leminv
 Tacinterp
+Evar_tactics
 Autorewrite
 Decl_interp
 Decl_proof_instr