From c25d1d8967dbdadbad85e22c50e1b63f6091e1fe Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:38:52 +0000
Subject: Refine does beta-reductions.

To avoid the unpleasantness of having beta-redex in terms after an application of refine, refine is followed by lazy beta.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17006 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/extratactics.ml4 | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index e4bcf658ba..436e3bd5be 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -321,8 +321,19 @@ 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 }
+    ))
+
 TACTIC EXTEND refine
-  [ "refine" casted_open_constr(c) ] -> [ Tactics.New.refine c ]
+  [ "refine" casted_open_constr(c) ] -> [  refine c ]
 END
 
 let refine_tac = Tactics.New.refine
-- 
cgit v1.2.3