Module Flags
Global options of the system.
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 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 tof 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
onf x y z
, usewith_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 with_extra_values : 'c list Stdlib.ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
Temporarily extends the reference to a list