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

4 files changed, 6 insertions, 22 deletions

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.
 
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index c16445ba3c..2453cb39bf 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -64,11 +64,6 @@ val undo_todepth : int -> unit
    to put informations in coq prompt (in emacs mode). *)
 val current_proof_depth: unit -> int
 
-(** [set_undo (Some n)] used to set the size of the ``undo'' stack. 
-    These function now do nothing and will disapear. *)
-val set_undo : int option -> unit
-val get_undo : unit -> int option
-
 (** {6 ... } *)
 (** [start_proof s str env t hook tac] starts a proof of name [s] and
     conclusion [t]; [hook] is optionally a function to be applied at
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 21ecdd5b05..6d342b7ca6 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -324,7 +324,6 @@ let init arglist =
         (print_string (String.concat "\n" foreign_args); exit 0);
       if !ide_slave then begin
         Flags.make_silent true;
-        Pfedit.set_undo (Some 5000);
         Ide_slave.init_stdout ()
       end;
       if_verbose print_header ();
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index b5484d40f3..465302a234 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -933,13 +933,16 @@ let _ =
       optread  = (fun _ -> not (Vm.transp_values ()));
       optwrite = (fun b -> Vm.set_transp_values (not b)) }
 
+(* No more undo limit in the new proof engine.
+   The command still exists for compatibility (e.g. with ProofGeneral) *)
+
 let _ =
   declare_int_option
     { optsync  = false;
-      optname  = "the undo limit";
+      optname  = "the undo limit (OBSOLETE)";
       optkey   = ["Undo"];
-      optread  = Pfedit.get_undo;
-      optwrite = Pfedit.set_undo }
+      optread  = (fun _ -> None);
+      optwrite = (fun _ -> ()) }
 
 let _ =
   declare_int_option