diff options
author | 2013-11-02 15:39:54 +0000 | |
---|---|---|
committer | 2013-11-02 15:39:54 +0000 | |
commit | c9504af26647ab745dc22811a2db8058e0b66632 (patch) | |
tree | 753c2029810002b23946636a3add74aacf86566c /doc/refman | |
parent | 8d68ee674daa5deaa327b80e75f01876ef6ea9a0 (diff) |
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
Diffstat (limited to 'doc/refman')
-rw-r--r-- | doc/refman/RefMan-tac.tex | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2c77af218..81e7db6dc 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} |