From 98db1b73f6ab89763ef386a2055528db91e4e152 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 5 Sep 2011 16:47:01 +0000
Subject: 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
---
 doc/refman/RefMan-pro.tex | 13 -------------
 1 file changed, 13 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/RefMan-pro.tex b/doc/refman/RefMan-pro.tex
index d73ab5d2ce..c781c82747 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.
 
-- 
cgit v1.2.3