diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 6 |
1 files changed, 1 insertions, 5 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index c05fc829e4..3e72816db9 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -199,13 +199,9 @@ and turns it into a goal. \subsection[\tt Undo.]{\tt Undo.\comindex{Undo}} -This command cancels the effect of the last tactic command. Thus, it +This command cancels the effect of the last command. Thus, it backtracks one step. -\begin{ErrMsgs} -\item \errindex{No focused proof (No proof-editing in progress)} -\end{ErrMsgs} - \begin{Variants} \item {\tt Undo {\num}.} |