package coq-core

You can search for identifiers within the package.

in-package search v0.2.0

The Coq Proof Assistant -- Core Binaries and Tools

Install

Dune Dependency

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

Authors

T

The Coq development team, INRIA, CNRS, and contributors

Maintainers

T

The Coq development team <coqdev@inria.fr>

Sources

coq-8.20.0.tar.gz

md5=66e57ea55275903bef74d5bf36fbe0f1

sha512=1a7eac6e2f58724a3f9d68bbb321e4cfe963ba1a5551b9b011db4b3f559c79be433d810ff262593d753770ee41ea68fbd6a60daa1e2319ea00dff64c8851d70b

doc/coq-core.lib/CDebug/index.html

Module `CDebug`Source

Sourcetype flag

Sourcetype t = (unit -> Pp.t) -> unit

Sourceval create : name:string -> unit -> t

Creates a debug component, which may be used to print debug messages.

A debug component is named by the string name. It is either active or inactive.

The special component "all" may be used to control all components.

There is also a special component "backtrace" to control backtrace recording.

Sourceval create_full : name:string -> unit -> flag * t

Useful when interacting with a component from code, typically when doing something more complicated than printing.

Note that the printer function prints some metadata compared to fun pp -> if get_flag flag then Feedback.msg_debug (pp ())

Sourceval get_flag : flag -> bool

Sourceval set_flag : flag -> bool -> unit

Sourceval get_flags : unit -> string

get_flags and set_flags use the user syntax: a comma separated list of activated "component" and "-component"s. get_flags starts with "all" or "-all" and lists all components after it (even if redundant).

Sourceval set_flags : string -> unit

Components not mentioned are not affected (use the "all" component at the start if you want to reset everything).

Sourceval set_debug_all : bool -> unit

Sourceval misc : flag

Sourceval pp_misc : t