package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac_plugin.Tactic_debugSource

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 =
  1. | DebugOn of int
  2. | DebugOff

Debug information

Prints the state and waits

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

Initializes debugger

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.

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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct