From 55bddb4bf35fa68318aa57a5fa8a113d1fe51159 Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Wed, 22 Feb 2017 02:31:16 +0100
Subject: [flags] Documentation and a minor tweak.

Mostly documentation and making a couple of local flags, local.
---
 vernac/vernacentries.ml | 18 ------------------
 1 file changed, 18 deletions(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5e5df99709..89d069e804 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1358,15 +1358,6 @@ let _ =
       optread  = (fun () -> !Flags.raw_print);
       optwrite = (fun b -> Flags.raw_print := b) }
 
-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;
@@ -1417,15 +1408,6 @@ let _ =
       optread  = (fun _ -> None);
       optwrite = (fun _ -> ()) }
 
-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;
-- 
cgit v1.2.3