package coq-core

  1. Overview
  2. Docs
The Coq Proof Assistant -- Core Binaries and Tools

Install 

dune-project
 Dependency

coq.inria.fr Readme Edit opam file Versions (11)

Authors

  1. T
    The Coq development team, INRIA, CNRS, and contributors

Maintainers

  1. T
    The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.1.tar.gz
md5=0cfaa70f569be9494d24c829e6555d46
sha512=8ee967c636b67b22a4f34115871d8f9b9114df309afc9ddf5f61275251088c6e21f6cf745811df75554d30f4cebb6682f23eeb2e88b771330c4b60ce3f6bf5e2

doc/coq-core.vernac/Topfmt/index.html

Module TopfmtSource

Console printing options

Sourcetype pp_global_params = {
  1. margin : int;
  2. max_indent : int;
  3. max_depth : int;
  4. ellipsis : string;
}
Sourceval set_dflt_gp : Format.formatter -> unit
Output functions of pretty-printing.
Sourceval with_output_to : out_channel -> Format.formatter
For parametrization through vernacular.
Sourceval set_depth_boxes : int option -> unit
Sourceval get_depth_boxes : unit -> int option
Sourceval set_margin : int option -> unit
Sourceval get_margin : unit -> int option
Sourceval std_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit

Console display of feedback, we may add some location information

Sourceval emacs_logger : ?pre_hdr:Pp.t -> Feedback.level -> Pp.t -> unit
Sourceval default_styles : unit -> unit

Color output

Sourceval parse_color_config : string -> unit
Sourceval dump_tags : unit -> (string * Terminal.style) list
Sourceval set_emacs_print_strings : unit -> unit
Sourceval init_terminal_output : color:bool -> unit

Initialization of interpretation of tags

Error printing

Sourcetype execution_phase =
  1. | ParsingCommandLine
  2. | Initialization
  3. | LoadingPrelude
  4. | LoadingRcFile
  5. | InteractiveLoop
  6. | CompilationPhase
Sourceval in_phase : phase:execution_phase -> ('a -> 'b) -> 'a -> 'b
Sourceval pr_phase : ?loc:Loc.t -> unit -> Pp.t option
Sourceval print_err_exn : exn -> unit
Sourceval with_output_to_file : string -> ('a -> 'b) -> 'a -> 'b

with_output_to_file file f x executes f x with logging redirected to a file file

Sourceval pr_cmd_header : Vernacexpr.vernac_control -> Pp.t