package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type

TODO: Move those definitions somewhere sensible

val 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

type debug_info =
  1. | DebugOn of int
  2. | DebugOff

Debug information

Prints the state and waits

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

Initializes debugger

Prints a constr

Prints the pattern rule

Prints a matched hypothesis

Prints the matched conclusion

val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t

Prints a success message when the goal has been matched

Prints a failure message for an hypothesis pattern

val db_matching_failure : debug_info -> unit Proofview.NonLogical.t

Prints a matching failure message for a rule

val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t

Prints an evaluation failure message for a rule

val explain_logic_error : exn -> Pp.t

An exception handler

val 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.

val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t

Prints a logic failure message for a rule

Check for/process idtac breakpoint

val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_stack -> Pp.t Loc.located
val defer_output : (unit -> Pp.t) -> unit Proofview.NonLogical.t

Prints a message only if debugger stops at the next step

val push_chunk : Tacexpr.ltac_trace -> unit

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

val pop_chunk : unit -> unit

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