Module `Flags`

Global options of the system.

val async_proofs_worker_id : string Stdlib.ref: Async-related flags

val async_proofs_is_worker : unit -> bool
val load_vos_libraries : bool Stdlib.ref: Flag to indicate that .vos files should be loaded for dependencies instead of .vo files. Used by -vos and -vok options.

val xml_debug : bool Stdlib.ref: Debug flags

val in_debugger : bool Stdlib.ref

val in_toplevel : bool Stdlib.ref

val in_synterp_phase : bool Stdlib.ref

val raw_print : bool Stdlib.ref

val beautify : bool Stdlib.ref

val beautify_file : bool Stdlib.ref

val quiet : bool Stdlib.ref

val silently : ('a -> 'b) -> 'a -> 'b

val verbosely : ('a -> 'b) -> 'a -> 'b

val if_silent : ('a -> unit) -> 'a -> unit

val if_verbose : ('a -> unit) -> 'a -> unit

val warn : bool Stdlib.ref

val make_warn : bool -> unit

val if_warn : ('a -> unit) -> 'a -> unit

val with_modified_ref : 'c Stdlib.ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b

with_modified_ref r nf f x Temporarily modify a reference in the call to f x . Be very careful with these functions, it is very easy to fall in the typical problem with effects:

with_modified_ref r nf f x y != with_modified_ref r nf (f x) y

val with_option : bool Stdlib.ref -> ('a -> 'b) -> 'a -> 'b: Temporarily activate an option (to activate option o on f x y z, use with_option o (f x y) z)

val with_options : bool Stdlib.ref list -> ('a -> 'b) -> 'a -> 'b: As with_option, but on several flags.

val without_option : bool Stdlib.ref -> ('a -> 'b) -> 'a -> 'b: Temporarily deactivate an option

val with_extra_values : 'c list Stdlib.ref -> 'c list -> ('a -> 'b) -> 'a -> 'b: Temporarily extends the reference to a list

val set_inline_level : int -> unit: Level of inlining during a functor application

val get_inline_level : unit -> int
val default_inline_level : int
val profile_ltac : bool Stdlib.ref: Global profile_ltac flag

val profile_ltac_cutoff : float Stdlib.ref