From c9504af26647ab745dc22811a2db8058e0b66632 Mon Sep 17 00:00:00 2001
From: aspiwack
Date: Sat, 2 Nov 2013 15:39:54 +0000
Subject: 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
---
 doc/refman/RefMan-tac.tex | 12 ++++++++++++
 1 file changed, 12 insertions(+)

(limited to 'doc')

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}
-- 
cgit v1.2.3