diff options
| author |  Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-08 10:20:57 +0200 |
|---|---|---|
| committer | Arnaud Spiwack <arnaud@spiwack.net> | 2014-09-08 10:58:23 +0200 |
| commit | 656fc30fb1279c4b5a0d196cb559707df74d894d (patch) | |
| tree | 43c78b7f621427103d654ffd106858b6976eff0e /doc | |
| parent | f815118ceec3b9adb8a24f34a7361fe14075ed53 (diff) | |
Doc: [revgoals].
Diffstat (limited to 'doc')
| -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 214e750bc..2bbeb3b1a 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}} |