From e875e90d1d90aec22e6f206f04c4941cb5a3bcd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 30 Nov 2013 19:34:46 +0100
Subject: Fixing ltac constr variable handling in refine.

---
 tactics/extratactics.ml4 | 16 ++++++++++------
 1 file changed, 10 insertions(+), 6 deletions(-)

(limited to 'tactics')

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 18326435c6..2e753e0cce 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 ]
-- 
cgit v1.2.3