package coq

  1. Overview
  2. Docs
Legend:
Library
Module
Module type
Parameter
Class
Class type
val async_proofs_worker_id : string ref
val async_proofs_is_worker : unit -> bool
val load_vos_libraries : bool ref
val debug : bool ref
val xml_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
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 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 get_native_compiler : unit -> bool
val set_native_compiler : bool -> unit
val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
val profile_ltac : bool ref
val profile_ltac_cutoff : float ref