Module Ltac_plugin.Tactic_debug

val ltac_trace_info : Tacexpr.ltac_trace Exninfo.t
type debug_info =
| DebugOn of int
| DebugOff

Debug information

val debug_prompt : int -> Tacexpr.glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic

Prints the state and waits

val db_initialize : 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 db_pattern_rule : debug_info -> Environ.env -> Evd.evar_map -> int -> (Genintern.glob_constr_and_expr * Pattern.constr_pattern, Tacexpr.glob_tactic_expr) Tacexpr.match_rule -> unit Proofview.NonLogical.t

Prints the pattern rule

val db_matched_hyp : debug_info -> Environ.env -> Evd.evar_map -> (Names.Id.t * EConstr.constr option * EConstr.constr) -> Names.Name.t -> unit Proofview.NonLogical.t

Prints a matched hypothesis

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

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

val db_hyp_pattern_failure : debug_info -> Environ.env -> Evd.evar_map -> (Names.Name.t * Pattern.constr_pattern Tacexpr.match_pattern) -> unit Proofview.NonLogical.t

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

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

Prints a logic failure message for a rule

val extract_ltac_trace : ?⁠loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t option Loc.located