Module Flags

Global options of the system.

WARNING: don't add new entries to this file!

This file is own its way to deprecation in favor of a purely functional state, but meanwhile it will contain options that are truly global to the system such as debug

If you are thinking about adding a global flag, well, just don't. First of all, options make testins exponentially more expensive, due to the growth of flag combinations. So please make some effort in order for your idea to work in a configuration-free manner.

If you absolutely must pass an option to your new system, then do so as a functional argument so flags are exposed to unit testing. Then, register such parameters with the proper state-handling mechanism of the top-level subsystem of Coq.

Command-line flags

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_ml_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 record_comments : 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
val output_directory : CUnix.physical_path option Stdlib.ref

Default output directory

val test_mode : bool Stdlib.ref

Flag set when the test-suite is called. Its only effect to display verbose information for Fail