package coq

  1. Overview
  2. Docs
package coq
Legend:
Library
Module
Module type
Parameter
Class
Class type
val ltac_trace_info : Tacexpr.ltac_trace Exninfo.t
type debug_info =
  1. | DebugOn of int
  2. | DebugOff
val debug_prompt : int -> Tacexpr.glob_tactic_expr -> (debug_info -> 'a Proofview.tactic) -> 'a Proofview.tactic
val db_initialize : unit Proofview.NonLogical.t
val db_mc_pattern_success : debug_info -> unit Proofview.NonLogical.t
val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
val db_eval_failure : debug_info -> Pp.t -> unit Proofview.NonLogical.t
val explain_logic_error : exn -> Pp.t
val explain_logic_error_no_anomaly : exn -> Pp.t
val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
val extract_ltac_trace : ?loc:Loc.t -> Tacexpr.ltac_trace -> Pp.t Loc.located
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