package coq

You can search for identifiers within the package.

in-package search v0.2.0

Formal proof management system

Install

Dune Dependency

coq.inria.fr Edit opam file Versions (38)

Authors

T

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

Maintainers

C

coqdev@inria.fr

Sources

coq-8.16.1.tar.gz

sha256=583471c8ed4f227cb374ee8a13a769c46579313d407db67a82d202ee48300e4b

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

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