Fixing ltac constr variable handling in refine.

3 files changed, 16 insertions, 11 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ae42acf18..43d7b3579 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -242,7 +242,7 @@ module Refinable = struct
   (* spiwack: it is not entirely satisfactory to have this function here. Plus it is
       a bit hackish. However it does not seem possible to move it out until
       pretyping is defined as some proof procedure. *)
-  let constr_of_raw handle check_type resolve_classes rawc = (); fun env rdefs gl info ->
+  let constr_of_raw handle check_type resolve_classes lvar rawc = (); fun env rdefs gl info ->
     (* We need to keep trace of what [rdefs] was originally*)
     let init_defs = !rdefs in
     (* if [check_type] is true, then creates a type constraint for the
@@ -253,9 +253,10 @@ module Refinable = struct
     let flags =
       if resolve_classes then Pretyping.all_no_fail_flags
       else Pretyping.no_classes_no_fail_inference_flags in
-    let open_constr =
-      Pretyping.understand_tcc_evars ~flags rdefs env ~expected_type:tycon rawc
+    let (sigma, open_constr) =
+      Pretyping.understand_ltac flags !rdefs env lvar tycon rawc
     in
+    let () = rdefs := sigma in
     let () = update_handle handle init_defs !rdefs in
     open_constr
 
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 1f04ce8c1..013b3199a 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -93,8 +93,8 @@ module Refinable : sig
       The principal argument is a [glob_constr] which is then pretyped in the
       context of a term, the remaining evars are registered to the handle.
       It is the main component of the toplevel refine tactic.*)
-  val constr_of_raw : 
-    handle -> bool -> bool -> Glob_term.glob_constr -> Term.constr sensitive
+  val constr_of_raw : handle -> bool -> bool -> Pretyping.ltac_var_map ->
+    Glob_term.glob_constr -> Term.constr sensitive
 
   (* [constr_of_open_constr h check_type] transforms an open constr into a 
      goal-sensitive constr, adding the undefined variables to the set of subgoals.
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 18326435c..2e753e0cc 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -336,12 +336,16 @@ let refine_red_flags =
 let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
 
 let refine_tac (ist, c) =
-  let c = Goal.Refinable.make begin fun h ->
-    Goal.Refinable.constr_of_raw h true true c
-  end in
-  Proofview.Goal.lift c >>= fun c ->
-  Proofview.tclSENSITIVE (Goal.refine c) <*>
-  Proofview.V82.tactic (reduce refine_red_flags refine_locs)
+  Proofview.Goal.enter (fun gl ->
+    let env = Proofview.Goal.env gl in
+    let constrvars = Tacinterp.extract_ltac_constr_values ist env in
+    let vars = (constrvars, ist.Geninterp.lfun) in
+    let c = Goal.Refinable.make begin fun h ->
+      Goal.Refinable.constr_of_raw h true true vars c
+    end in
+    Proofview.Goal.lift c >>= fun c ->
+    Proofview.tclSENSITIVE (Goal.refine c) <*>
+    Proofview.V82.tactic (reduce refine_red_flags refine_locs))
 
 TACTIC EXTEND refine
   [ "refine" glob(c) ] -> [  refine_tac c ]