diff options
| author | Arnaud Spiwack | 2014-09-08 10:20:57 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2014-09-08 10:58:23 +0200 |
| commit | 656fc30fb1279c4b5a0d196cb559707df74d894d (patch) | |
| tree | 43c78b7f621427103d654ffd106858b6976eff0e | |
| parent | f815118ceec3b9adb8a24f34a7361fe14075ed53 (diff) | |
Doc: [revgoals].
| -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}} |