package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 we_are_parsing : bool ref
val raw_print : bool ref
type compat_version =
  1. | V8_7
  2. | V8_8
  3. | 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