From 8ead702b4f0ec5e0fecfc5de68f7ce86f56b20fe Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:40:29 +0000
Subject: Refine: Tactics.New.refine does beta-reduction.

Previously I had wrapped Tactics.New.refine with extra
beta-reduction in extratactics.ml4, that is, only for Ltac.
Ocaml plugins saw the version without reduction.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17019 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 14 ++------------
 tactics/tactics.ml       |  9 ++++++++-
 2 files changed, 10 insertions(+), 13 deletions(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e45c2170a5..e6578ce52d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -321,23 +321,13 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-open Genredexpr
-open Locus
 
-let refine c =
-  Proofview.tclTHEN
-    (Tactics.New.refine c)
-    (Proofview.V82.tactic (Tactics.reduce
-       (Lazy {rBeta=true;rIota=false;rZeta=false;rDelta=false;rConst=[]})
-       {onhyps=None; concl_occs=AllOccurrences }
-    ))
+let refine_tac = Tactics.New.refine
 
 TACTIC EXTEND refine
-  [ "refine" casted_open_constr(c) ] -> [  refine c ]
+  [ "refine" casted_open_constr(c) ] -> [  refine_tac c ]
 END
 
-let refine_tac = Tactics.New.refine
-
 (**********************************************************************)
 (* Inversion lemmas (Leminv)                                          *)
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d1ba7756c..c933ec44e6 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3870,11 +3870,18 @@ module New = struct
 
   let exact_proof c = Proofview.V82.tactic (exact_proof c)
 
+  open Genredexpr
+  open Locus
+
   let refine c =
     let c = Goal.Refinable.make begin fun h ->
       Goal.Refinable.constr_of_open_constr h true c
     end in
     Proofview.Goal.lift c >>= fun c ->
-    Proofview.tclSENSITIVE (Goal.refine c)
+    Proofview.tclSENSITIVE (Goal.refine c) <*>
+    Proofview.V82.tactic (reduce
+       (Lazy {rBeta=true;rIota=false;rZeta=false;rDelta=false;rConst=[]})
+       {onhyps=None; concl_occs=AllOccurrences }
+    )
 
 end
-- 
cgit v1.2.3