[flags] Documentation and a minor tweak.

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

1 files changed, 18 insertions, 5 deletions

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 *)