[flags] Documentation and a minor tweak.

Mostly documentation and making a couple of local flags, local.

1 files changed, 0 insertions, 18 deletions

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5e5df9970..89d069e80 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1362,15 +1362,6 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "record printing";
-      optkey   = ["Printing";"Records"];
-      optread  = (fun () -> !Flags.record_print);
-      optwrite = (fun b -> Flags.record_print := b) }
-
-let _ =
-  declare_bool_option
-    { optsync  = true;
-      optdepr  = false;
       optname  = "use of the program extension";
       optkey   = ["Program";"Mode"];
       optread  = (fun () -> !Flags.program_mode);
@@ -1419,15 +1410,6 @@ let _ =
 
 let _ =
   declare_int_option
-    { optsync  = false;
-      optdepr  = false;
-      optname  = "the hypotheses limit";
-      optkey   = ["Hyps";"Limit"];
-      optread  = Flags.print_hyps_limit;
-      optwrite = Flags.set_print_hyps_limit }
-
-let _ =
-  declare_int_option
     { optsync  = true;
       optdepr  = false;
       optname  = "the printing depth";