Tac2bt (coq-core.Ltac2_plugin.Tac2bt)

val backtrace : Tac2expr.backtrace Exninfo.t

val get_backtrace : Tac2expr.backtrace Proofview.tactic

val with_frame : Tac2expr.frame -> 'a Proofview.tactic -> 'a Proofview.tactic

val print_ltac2_backtrace : bool Stdlib.ref

val pr_frame_hook : (Tac2expr.frame -> Pp.t) Hook.t