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

1 files changed, 13 insertions, 4 deletions

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}