package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val boot : bool Pervasives.ref
val record_aux_file : bool Pervasives.ref
val test_mode : bool Pervasives.ref
val async_proofs_worker_id : string Pervasives.ref
val async_proofs_is_worker : unit -> bool
val debug : bool Pervasives.ref
val in_debugger : bool Pervasives.ref
val in_toplevel : bool Pervasives.ref
val profile : bool
val ide_slave : bool Pervasives.ref
val we_are_parsing : bool Pervasives.ref
val raw_print : bool Pervasives.ref
val univ_print : bool Pervasives.ref
type compat_version =
  1. | V8_6
  2. | V8_7
  3. | Current
val compat_version : compat_version Pervasives.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 Pervasives.ref
val beautify_file : bool Pervasives.ref
val quiet : bool Pervasives.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 Pervasives.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 Pervasives.ref
val make_warn : bool -> unit
val if_warn : ('a -> unit) -> 'a -> unit
val with_modified_ref : 'c Pervasives.ref -> ('c -> 'c) -> ('a -> 'b) -> 'a -> 'b
val with_option : bool Pervasives.ref -> ('a -> 'b) -> 'a -> 'b
val with_options : bool Pervasives.ref list -> ('a -> 'b) -> 'a -> 'b
val without_option : bool Pervasives.ref -> ('a -> 'b) -> 'a -> 'b
val with_extra_values : 'c list Pervasives.ref -> 'c list -> ('a -> 'b) -> 'a -> 'b
val browser_cmd_fmt : string
val is_standard_doc_url : string -> bool
val coqlib_spec : bool Pervasives.ref
val coqlib : string Pervasives.ref
val set_inline_level : int -> unit
val get_inline_level : unit -> int
val default_inline_level : int
val output_native_objects : bool Pervasives.ref
val print_mod_uid : bool Pervasives.ref
val profile_ltac : bool Pervasives.ref
val profile_ltac_cutoff : float Pervasives.ref
val dump_bytecode : bool Pervasives.ref
val set_dump_bytecode : bool -> unit
val get_dump_bytecode : unit -> bool
val dump_lambda : bool Pervasives.ref
val set_dump_lambda : bool -> unit
val get_dump_lambda : 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