Adds a shelve tactic.

The shelve tactic puts all the focused goals out of sight. They can be later recalled by the Unshelve command.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17013 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 12 insertions, 0 deletions

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index 2c77af2183..81e7db6dc0 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -4614,6 +4614,18 @@ intros; fourier.
 Reset Initial.
 \end{coq_eval}
 
+\section{Non-logical tactics}
+\subsection[\tt shelve]{\tt shelve\tacindex{shelve}\label{shelve}}
+
+This tactic moves all goals under focus to a shelf. While on the shelf, goals
+will not be focused on. They can be solved by unification, or they can be called
+back into focus with the command {\tt Unshelve} (Section~\ref{unshelve}).
+
+\subsection[\tt Unshelve]{\tt Unshelve\comindex{Unshelve}\label{unshelve}}
+
+This command moves all the goals on the shelf (see Section~\ref{shelve}) from the
+shelf into focus, by appending them to the end of the current list of focused goals.
+
 
 \section{Simple tactic macros}
 \index{Tactic macros}