Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".

3 files changed, 30 insertions, 12 deletions

diff --git a/CHANGES b/CHANGES
index a3cec81c1a..df2fc967dd 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,11 +1,12 @@
 Changes from V8.5beta3
 ======================
 
-Vernacular commands
-- Flag -compat 8.4 now loads Coq.Compat.Coq84. The standard way of putting Coq
-  in v8.4 compatibility mode is to pass the command line flag "-compat 8.4". It
-  can be followed by "-require Coq.Compat.AdmitAxiom" if 8.4 behavior of admit is
-  needed, in which case it uses an axiom.
+Tools
+
+- Flag "-compat 8.4" now loads Coq.Compat.Coq84. The standard way of
+  putting Coq in v8.4 compatibility mode is to pass the command line flag
+  "-compat 8.4". It can be followed by "-require Coq.Compat.AdmitAxiom"
+  if the 8.4 behavior of admit is needed, in which case it uses an axiom.
 
 Specification language
 
@@ -21,6 +22,9 @@ Tactics
   introducing along pattern p changed to p%c1..%cn. The feature and
   syntax are in experimental stage.
 - "Proof using" does not clear unused section variables.
+- "refine" has been changed back to the 8.4 behavior of shelving subgoals
+  that occur in other subgoals. The "refine" tactic of 8.5beta2 has been
+  renamed "simple refine"; it does not shelve any subgoal.
 
 Changes from V8.5beta2 to V8.5beta3
 ===================================
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 3a3877105b..d90a027295 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -219,8 +219,10 @@ difference: the user can leave some holes (denoted by \texttt{\_} or
 {\tt (\_:\type)}) in the term. {\tt refine} will generate as
 many subgoals as there are holes in the term. The type of holes must be
 either synthesized by the system or declared by an
-explicit cast like \verb|(_:nat->Prop)|. This low-level
-tactic can be useful to advanced users.
+explicit cast like \verb|(_:nat->Prop)|. Any subgoal that occurs in other
+subgoals is automatically shelved, as if calling {\tt shelve\_unifiable}
+(see Section~\ref{shelve}).
+This low-level tactic can be useful to advanced users.
 
 \Example
 
@@ -256,6 +258,13 @@ Defined.
   which type cannot be inferred. Put a cast around it.
 \end{ErrMsgs}
 
+\begin{Variants}
+\item {\tt simple refine \term}\tacindex{simple refine}
+
+  This tactic behaves like {\tt refine}, but it does not shelve any
+  subgoal. It does not perform any beta-reduction either.
+\end{Variants}
+
 \subsection{\tt apply \term}
 \tacindex{apply}
 \label{apply}
@@ -4964,8 +4973,8 @@ back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
 \begin{Variants}
   \item \texttt{shelve\_unifiable}\tacindex{shelve\_unifiable}
 
-    Shelves only these goals under focused which are mentioned in other goals.
-    Goals which appear in the type of other goals can be solve by unification.
+    Shelves only the goals under focus that are mentioned in other goals.
+    Goals that appear in the type of other goals can be solved by unification.
 
 \Example
 \begin{coq_example}
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index ca65f08ec0..e06997029d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -345,7 +345,7 @@ END
 (**********************************************************************)
 (* Refine                                                             *)
 
-let refine_tac {Glob_term.closure=closure;term=term} =
+let refine_tac simple {Glob_term.closure=closure;term=term} =
   Proofview.Goal.nf_enter begin fun gl ->
     let concl = Proofview.Goal.concl gl in
     let env = Proofview.Goal.env gl in
@@ -357,11 +357,16 @@ let refine_tac {Glob_term.closure=closure;term=term} =
       Pretyping.ltac_idents = closure.Glob_term.idents;
     } in
     let update evd = Pretyping.understand_ltac flags env evd lvar tycon term in
-    Tactics.New.refine ~unsafe:false update <*> Proofview.shelve_unifiable
+    let refine = Proofview.Refine.refine ~unsafe:false update in
+    if simple then refine
+    else refine <*>
+           Tactics.New.reduce_after_refine <*>
+           Proofview.shelve_unifiable
   end
 
 TACTIC EXTEND refine
-  [ "refine" uconstr(c) ] -> [  refine_tac c ]
+| [ "refine" uconstr(c) ] -> [ refine_tac false c ]
+| [ "simple" "refine" uconstr(c) ] -> [ refine_tac true c ]
 END
 
 (**********************************************************************)