diff options
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 18 |
1 files changed, 18 insertions, 0 deletions
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 214e750bc1..2bbeb3b1ab 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -4776,6 +4776,24 @@ all: swap 1 -1. Reset Initial. \end{coq_eval} +\subsection[\tt revgoals]{\tt revgoals\tacindex{revgoals}} + +This tactics reverses the list of the focused goals. + +\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: revgoals. +\end{coq_example} + +\begin{coq_eval} +Reset Initial. +\end{coq_eval} + \subsection[\tt shelve]{\tt shelve\tacindex{shelve}\label{shelve}} |