diff options
| -rw-r--r-- | CHANGES | 1 | ||||
| -rw-r--r-- | doc/refman/RefMan-pro.tex | 6 |
2 files changed, 2 insertions, 5 deletions
@@ -59,6 +59,7 @@ Vernacular commands Coq: terms, modules, tactics, etc. The old behaviour of the command can be retrieved using the "Locate Term" command. - New "Derive" command to help writing program by derivation. +- "Undo" undoes any command, not just tactics. Specification Language 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}.} |