diff options
author | 2011-09-05 16:47:01 +0000 | |
---|---|---|
committer | 2011-09-05 16:47:01 +0000 | |
commit | 98db1b73f6ab89763ef386a2055528db91e4e152 (patch) | |
tree | 1743e12160bef3ace6ea46fa00f5618df65ebecc /doc | |
parent | e4c505927b0ebe06f87ecc14567431822e8e0b5c (diff) |
Remove code concerning the obsolete Set/Unset Undo
Even if they are no-ops now, the commands Set/Unset Undo themselves
are kept for compatibility, in particular to avoid error messages
or warnings during the initialization of ProofGeneral.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14451 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'doc')
-rw-r--r-- | doc/refman/RefMan-pro.tex | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex index d73ab5d2c..c781c8274 100644 --- a/doc/refman/RefMan-pro.tex +++ b/doc/refman/RefMan-pro.tex @@ -211,7 +211,6 @@ backtracks one step. \begin{ErrMsgs} \item \errindex{No focused proof (No proof-editing in progress)} -\item \errindex{Undo stack would be exhausted} \end{ErrMsgs} \begin{Variants} @@ -222,18 +221,6 @@ backtracks one step. \end{Variants} -\subsection[\tt Set Undo {\num}.]{\tt Set Undo {\num}.\comindex{Set Undo}} - -This command changes the maximum number of {\tt Undo}'s that will be -possible when doing a proof. It only affects proofs started after -this command, such that if you want to change the current undo limit -inside a proof, you should first restart this proof. - -\subsection[\tt Unset Undo.]{\tt Unset Undo.\comindex{Unset Undo}} - -This command resets the default number of possible {\tt Undo} commands -(which is currently 12). - \subsection[\tt Restart.]{\tt Restart.\comindex{Restart}} This command restores the proof editing process to the original goal. |