coq 8.7.2 · OCaml Package

val boot : bool ref

val load_init : bool ref

val batch_mode : bool ref

type compilation_mode =

| BuildVo
| BuildVio
| Vio2Vo

val compilation_mode : compilation_mode ref

val compilation_output_name : string option ref

val test_mode : bool ref

type async_proofs =

| APoff
| APonLazy
| APon

val async_proofs_mode : async_proofs ref

type cache =

| Force

val async_proofs_cache : cache option ref

val async_proofs_n_workers : int ref

val async_proofs_n_tacworkers : int ref

val async_proofs_private_flags : string option ref

val async_proofs_is_worker : unit -> bool

val async_proofs_is_master : unit -> bool

val async_proofs_full : bool ref

val async_proofs_never_reopen_branch : bool ref

val async_proofs_flags_for_workers : string list ref

val async_proofs_worker_id : string ref

type priority =

| Low
| High

val async_proofs_worker_priority : priority ref

val string_of_priority : priority -> string

val priority_of_string : string -> priority

type tac_error_filter = [

| `All
| `None
| `Only of string list

]

val async_proofs_tac_error_resilience : tac_error_filter ref

val async_proofs_cmd_error_resilience : bool ref

val async_proofs_delegation_threshold : float ref

val debug : bool ref

val in_debugger : bool ref

val in_toplevel : bool ref

val stm_debug : bool ref

val profile : bool

val xml_export : bool ref

val ide_slave : bool ref

val ideslave_coqtop_flags : string option ref

val time : bool ref

val we_are_parsing : bool ref

val raw_print : bool ref

val univ_print : bool ref

type compat_version =

| VOld
| V8_5
| V8_6
| 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_silent : bool -> unit

deprecated Please use Flags.quiet

val is_silent : unit -> bool

deprecated Please use Flags.quiet

val is_verbose : unit -> bool

deprecated Please use Flags.quiet

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_flag : bool -> unit

val use_polymorphic_flag : 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_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 ocamlfind_spec : bool ref

val ocamlfind : string ref

val camlp4bin_spec : bool ref

val camlp4bin : string ref

val set_inline_level : int -> unit

val get_inline_level : unit -> int

val default_inline_level : int

val native_compiler : bool ref

val print_mod_uid : bool ref

val tactic_context_compat : 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

package coq