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

1 files changed, 8 insertions, 1 deletions

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