package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val start_dump_glob : vfile:string -> vofile:string -> unit
val end_dump_glob : unit -> unit
val dump : unit -> bool
type glob_output =
  1. | NoGlob
  2. | Feedback
  3. | MultFiles
  4. | File of string
val push_output : glob_output -> unit

push_output o temporarily overrides the output location to o. The original output can be restored using pop_output

val pop_output : unit -> unit

Restores the original output that was overridden by push_output

val pause : unit -> unit

Alias for push_output NoGlob

val continue : unit -> unit

Deprecated alias for pop_output

  • deprecated Use pop_output
val add_glob : ?loc:Loc.t -> Names.GlobRef.t -> unit
val add_glob_kn : ?loc:Loc.t -> Names.KerName.t -> unit
val dump_definition : Names.lident -> bool -> string -> unit
val dump_moddef : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_modref : ?loc:Loc.t -> Names.ModPath.t -> string -> unit
val dump_reference : ?loc:Loc.t -> string -> string -> string -> unit
val dump_secvar : ?loc:Loc.t -> Names.Id.t -> unit
val dump_libref : ?loc:Loc.t -> Names.DirPath.t -> string -> unit
val dump_notation_location : (int * int) list -> Constrexpr.notation -> (Notation.notation_location * Notation_term.scope_name option) -> unit
val dump_binding : ?loc:Loc.t -> string -> unit
val dump_notation : Constrexpr.notation CAst.t -> Notation_term.scope_name option -> bool -> unit
val dump_constraint : Names.lname -> bool -> string -> unit
val dump_string : string -> unit
val type_of_global_ref : Names.GlobRef.t -> string
val add_constant_kind : Names.Constant.t -> Decls.logical_kind -> unit

Registration of constant information

val constant_kind : Names.Constant.t -> Decls.logical_kind
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