From 8ead702b4f0ec5e0fecfc5de68f7ce86f56b20fe Mon Sep 17 00:00:00 2001
From: aspiwack <aspiwack@85f007b7-540e-0410-9357-904b9bb8a0f7>
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/tactics.ml | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tactics/tactics.ml')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d1ba7756..c933ec44e 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