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

Source

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

Source

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

Source

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

Prints the matched conclusion

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

Prints a success message when the goal has been matched

Source

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

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

Prints a matching failure message for a rule

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

Prints an evaluation failure message for a rule

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.

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

Prints a logic failure message for a rule

Source

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

Check for/process idtac breakpoint

Sourceval extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_stack -> Pp.t Loc.located

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

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac_plugin/Ltac_plugin/Tactic_debug/index.html

Module `Ltac_plugin.Tactic_debug`Source

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