From 2b7f460f32aca14bcb58cefbdc29ab39c14da5ff Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 25 Jul 2014 18:58:11 +0200
Subject: Document cycle tactic.

---
 doc/refman/RefMan-tac.tex | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index bee91c952f..59052fffa1 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
-- 
cgit v1.2.3