1 files changed, 0 insertions, 11 deletions
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index ef16df5b7..9978848ff 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1394,17 +1394,6 @@ let _ =
       optread  = (fun () -> !CClosure.share);
       optwrite = (fun b -> CClosure.share := b) }
 
-(* No more undo limit in the new proof engine.
-   The command still exists for compatibility (e.g. with ProofGeneral) *)
-
-let _ =
-  declare_int_option
-    { optdepr  = true;
-      optname  = "the undo limit (OBSOLETE)";
-      optkey   = ["Undo"];
-      optread  = (fun _ -> None);
-      optwrite = (fun _ -> ()) }
-
 let _ =
   declare_bool_option
     { optdepr  = false;