Module `Ltac_plugin.Tactic_debug`

val ltac_trace_info : Tacexpr.ltac_stack Exninfo.t

type debug_info = | DebugOn of int | DebugOff: Debug information

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

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

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

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_breakpoint : debug_info -> Names.lident Tacexpr.message_token list -> unit Proofview.NonLogical.t: Check for/process idtac breakpoint

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