coq 8.8.1 · OCaml Package

val boot : bool ref

val record_aux_file : bool ref

val test_mode : bool ref

val async_proofs_worker_id : string ref

val async_proofs_is_worker : unit -> bool

val debug : bool ref

val in_debugger : bool ref

val in_toplevel : bool ref

val profile : bool

val ide_slave : bool ref

val we_are_parsing : bool ref

val raw_print : bool ref

val univ_print : bool ref

type compat_version =

| V8_6
| V8_7
| Current

val compat_version : compat_version 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 ref

val beautify_file : bool ref

val quiet : bool 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 make_auto_intros : bool -> unit

val is_auto_intros : unit -> bool

val program_mode : bool ref

val is_program_mode : unit -> bool

val make_universe_polymorphism : bool -> unit

val is_universe_polymorphism : unit -> bool

val make_polymorphic_inductive_cumulativity : bool -> unit

val is_polymorphic_inductive_cumulativity : unit -> bool

val warn : bool ref

val make_warn : bool -> unit

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

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

val with_option : bool ref -> ('a -> 'b) -> 'a -> 'b

val with_options : bool ref list -> ('a -> 'b) -> 'a -> 'b

val without_option : bool ref -> ('a -> 'b) -> 'a -> 'b

val with_extra_values : 'c list ref -> 'c list -> ('a -> 'b) -> 'a -> 'b

val browser_cmd_fmt : string

val is_standard_doc_url : string -> bool

val coqlib_spec : bool ref

val coqlib : string ref

val set_inline_level : int -> unit

val get_inline_level : unit -> int

val default_inline_level : int

val output_native_objects : bool ref

val print_mod_uid : bool ref

val profile_ltac : bool ref

val profile_ltac_cutoff : float ref

val dump_bytecode : bool ref

val set_dump_bytecode : bool -> unit

val get_dump_bytecode : unit -> bool

val dump_lambda : bool ref

val set_dump_lambda : bool -> unit

val get_dump_lambda : unit -> bool

package coq