diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index bee91c952..59052fffa 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4626,6 +4626,28 @@ Reset Initial. \end{coq_eval} \section{Non-logical tactics} + +\subsection[\tt cycle \num]{\tt cycle \num\tacindex{cycle}} + +This tactic puts the {\num} first goals at the end of the list of +goals. If {\num} is negative, it will put the last $\left|\num\right|$ goals at +the begining of the list. + +\Example +\begin{coq_example*} +Parameter P : nat -> Prop. +Goal P 1 /\ P 2 /\ P 3 /\ P 4 /\ P 5. +\end{coq_example*} +\begin{coq_example} +repeat split. +all: cycle 2. +all: cycle -3. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + \subsection[\tt shelve]{\tt shelve\tacindex{shelve}\label{shelve}} This tactic moves all goals under focus to a shelf. While on the shelf, goals |