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 debug : bool Stdlib.ref

Debug flags

val in_debugger : bool Stdlib.ref
val in_toplevel : bool Stdlib.ref
val profile : bool
val we_are_parsing : bool Stdlib.ref
val raw_print : bool Stdlib.ref
type compat_version =
| V8_9
| V8_10
| Current
val compat_version : compat_version Stdlib.ref
val version_compare : compat_version -> compat_version -> int
val version_strictly_greater : compat_version -> bool
val version_less_or_equal : compat_version -> bool
val pr_version : compat_version -> string
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