package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val boot : bool ref
val load_init : bool ref
val batch_mode : bool ref
type compilation_mode =
  1. | BuildVo
  2. | BuildVio
  3. | Vio2Vo
val compilation_mode : compilation_mode ref
val compilation_output_name : string option ref
val test_mode : bool ref
type async_proofs =
  1. | APoff
  2. | APonLazy
  3. | APon
val async_proofs_mode : async_proofs ref
type cache =
  1. | 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 =
  1. | Low
  2. | High
val async_proofs_worker_priority : priority ref
val string_of_priority : priority -> string
val priority_of_string : string -> priority
type tac_error_filter = [
  1. | `All
  2. | `None
  3. | `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 =
  1. | VOld
  2. | V8_5
  3. | V8_6
  4. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct