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/ltac_plugin/Ltac_plugin/Tactic_debug/index.html

Module `Ltac_plugin.Tactic_debug`Source

TODO: Move those definitions somewhere sensible

Sourceval ltac_trace_info : Tacexpr.ltac_stack Exninfo.t

This module intends to be a beginning of debugger for tactic expressions. Currently, it is quite simple and we can hope to have, in the future, a more complete panel of commands dedicated to a proof assistant framework

Sourcetype debug_info =

| DebugOn of int
| DebugOff

Debug information

Source

val debug_prompt : 
  int ->
  Tacexpr.glob_tactic_expr ->
  (debug_info -> 'a Proofview.tactic) ->
  Geninterp.Val.t Names.Id.Map.t ->
  Tacexpr.ltac_trace option ->
  'a Proofview.tactic

Prints the state and waits

Sourceval db_initialize : bool -> unit Proofview.NonLogical.t

Initializes debugger

Source

val db_constr : 
  debug_info ->
  Environ.env ->
  Evd.evar_map ->
  EConstr.constr ->
  unit Proofview.NonLogical.t

Prints a constr

Sourceval explain_logic_error : exn -> Pp.t

An exception handler

Sourceval explain_logic_error_no_anomaly : exn -> Pp.t

For use in the Ltac debugger: some exception that are usually consider anomalies are acceptable because they are caught later in the process that is being debugged. One should not require from users that they report these anomalies.

Source

val db_breakpoint : 
  debug_info ->
  Names.lident Tacexpr.message_token list ->
  unit Proofview.NonLogical.t

Check for/process idtac breakpoint

Sourceval defer_output : (unit -> Pp.t) -> unit Proofview.NonLogical.t

Prints a message only if debugger stops at the next step

Sourceval push_chunk : Tacexpr.ltac_trace -> unit

Push a trace chunk (multiple frames) onto the trace chunk stack

Sourceval pop_chunk : unit -> unit

Pop a trace chunk (multiple frames) from the trace chunk stack

package coq-core

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tactic_debug/index.html

Module Ltac_plugin.Tactic_debugSource

Module `Ltac_plugin.Tactic_debug`Source