From d32bd531b00ee8916a003c0b62029ddffbccc35b Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Tue, 5 Aug 2014 12:17:31 +0200
Subject: The [refine] tactic now accepts [uconstr].

Arguments of refine can hence be built by tactics instead of given in their entirety in one go.---
 tactics/extratactics.ml4 | 12 ++++--------
 1 file changed, 4 insertions(+), 8 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index b9fac2ca72..9603064c1c 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -359,24 +359,20 @@ let refine_red_flags =
 
 let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
 
-let refine_tac (ist, c) =
-  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 refine_tac c =
     let c = Goal.Refinable.make begin fun h ->
       Goal.bind Goal.concl (fun concl ->
         let flags = Pretyping.all_no_fail_flags in
         let tycon = Pretyping.OfType concl in
-        Goal.Refinable.constr_of_raw h tycon flags vars c)
+        Goal.Refinable.constr_of_raw h tycon flags Id.Map.(empty,empty) c)
     end in
     Proofview.Goal.lift c begin fun c ->
       Proofview.tclSENSITIVE (Goal.refine c) <*>
       Proofview.V82.tactic (reduce refine_red_flags refine_locs)
-    end)
+    end
 
 TACTIC EXTEND refine
-  [ "refine" glob(c) ] -> [  refine_tac c ]
+  [ "refine" uconstr(c) ] -> [  refine_tac c ]
 END
 
 (**********************************************************************)
-- 
cgit v1.2.3