[flags] Documentation and a minor tweak.

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

5 files changed, 48 insertions, 33 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 925e9517c..5bf49b733 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -85,6 +85,20 @@ let without_specific_symbols l f =
 (**********************************************************************)
 (* Control printing of records *)
 
+(* Set Record Printing flag *)
+let record_print = ref true
+
+let _ =
+  let open Goptions in
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "record printing";
+      optkey   = ["Printing";"Records"];
+      optread  = (fun () -> !record_print);
+      optwrite = (fun b -> record_print := b) }
+
+
 let is_record indsp =
   try
     let _ = Recordops.lookup_structure indsp in
@@ -658,7 +672,7 @@ let rec extern inctx scopes vars r =
                    ()
                  else if PrintingConstructor.active (fst cstrsp) then
                    raise Exit
-                 else if not !Flags.record_print then
+                 else if not !record_print then
                    raise Exit;
 		 let projs = struc.Recordops.s_PROJ in
 		 let locals = struc.Recordops.s_PROJKIND in
diff --git a/lib/flags.ml b/lib/flags.ml
index ef5eddfb2..d87d9e729 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -95,7 +95,6 @@ let time = ref false
 
 let raw_print = ref false
 
-let record_print = ref true
 
 let univ_print = ref false
 
@@ -181,12 +180,6 @@ let warn = ref true
 let make_warn flag = warn := flag;  ()
 let if_warn f x = if !warn then f x
 
-(* The number of printed hypothesis in a goal *)
-
-let print_hyps_limit = ref (None : int option)
-let set_print_hyps_limit n = print_hyps_limit := n
-let print_hyps_limit () = !print_hyps_limit
-
 (* Flags for external tools *)
 
 let browser_cmd_fmt =
diff --git a/lib/flags.mli b/lib/flags.mli
index f5e1c96f9..c5c4a15aa 100644
--- a/lib/flags.mli
+++ b/lib/flags.mli
@@ -8,6 +8,8 @@
 
 (** Global options of the system. *)
 
+(** Command-line flags  *)
+
 val boot : bool ref
 val load_init : bool ref
 
@@ -16,8 +18,11 @@ type compilation_mode = BuildVo | BuildVio | Vio2Vo
 val compilation_mode : compilation_mode ref
 val compilation_output_name : string option ref
 
+(* Flag set when the test-suite is called. Its only effect to display
+   verbose information for `Fail` *)
 val test_mode : bool ref
 
+(** Async-related flags *)
 type async_proofs = APoff | APonLazy | APon
 val async_proofs_mode : async_proofs ref
 type cache = Force
@@ -47,18 +52,26 @@ val in_toplevel : bool ref
 val profile : bool
 
 (* Legacy flags *)
+
+(* -emacs option: printing includes emacs tags, will affect stm caching. *)
 val print_emacs : bool ref
+(* -xml option: xml hooks will be called *)
 val xml_export : bool ref
 
+(* -ide_slave: printing will be more verbose, will affect stm caching *)
 val ide_slave : bool ref
 val ideslave_coqtop_flags : string option ref
 
+(* -time option: every command will be wrapped with `Time` *)
 val time : bool ref
 
+(* development flag to detect race conditions, it should go away. *)
 val we_are_parsing : bool ref
 
+(* Set Printing All flag. For some reason it is a global flag *)
 val raw_print : bool ref
-val record_print : bool ref
+
+(* Univ print flag, never set anywere. Maybe should belong to Univ? *)
 val univ_print : bool ref
 
 type compat_version = V8_2 | V8_3 | V8_4 | V8_5 | V8_6 | Current
@@ -68,9 +81,12 @@ val version_strictly_greater : compat_version -> bool
 val version_less_or_equal : compat_version -> bool
 val pr_version : compat_version -> string
 
+(* Beautify command line flags, should move to printing? *)
 val beautify : bool ref
 val beautify_file : bool ref
 
+(* Silent/verbose, both actually controlled by a single flag so they
+   are mutually exclusive *)
 val make_silent : bool -> unit
 val is_silent : unit -> bool
 val is_verbose : unit -> bool
@@ -79,6 +95,7 @@ val verbosely : ('a -> 'b) -> 'a -> 'b
 val if_silent : ('a -> unit) -> 'a -> unit
 val if_verbose : ('a -> unit) -> 'a -> unit
 
+(* Miscellaneus flags for vernac *)
 val make_auto_intros : bool -> unit
 val is_auto_intros : unit -> bool
 
@@ -110,10 +127,6 @@ val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b
 (** Temporarily extends the reference to a list *)
 val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
 
-(** If [None], no limit *)
-val set_print_hyps_limit : int option -> unit
-val print_hyps_limit : unit -> int option
-
 (** Options for external tools *)
 
 (** Returns string format for default browser to use from Coq or CoqIDE *)
diff --git a/printing/printer.ml b/printing/printer.ml
index 5e7e9ce54..f00350c6a 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -365,8 +365,21 @@ let pr_context_limit_compact ?n env sigma =
 let pr_context_unlimited_compact env sigma =
   pr_context_limit_compact env sigma
 
-let pr_context_of env sigma =
-  match Flags.print_hyps_limit () with
+(* The number of printed hypothesis in a goal *)
+(* If [None], no limit *)
+let print_hyps_limit = ref (None : int option)
+
+let _ =
+  let open Goptions in
+  declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = (fun () -> !print_hyps_limit);
+      optwrite = (fun x -> print_hyps_limit := x) }
+
+let pr_context_of env sigma = match !print_hyps_limit with
   | None -> hv 0 (pr_context_limit_compact env sigma)
   | Some n -> hv 0 (pr_context_limit_compact ~n env sigma)
 
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";