Module Ltac2_plugin.Tac2entries

Toplevel definitions
val register_ltac : ?⁠local:bool -> ?⁠mut:bool -> Tac2expr.rec_flag -> (Names.lname * Tac2expr.raw_tacexpr) list -> unit
val register_type : ?⁠local:bool -> Tac2expr.rec_flag -> (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list -> unit
val register_primitive : ?⁠local:bool -> Names.lident -> Tac2expr.raw_typexpr -> Tac2expr.ml_tactic_name -> unit
val register_struct : ?⁠local:bool -> Tac2expr.strexpr -> unit
val register_notation : ?⁠local:bool -> Tac2expr.sexpr list -> int option -> Tac2expr.raw_tacexpr -> unit
val perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
Notations
type scope_rule =
| ScopeRule : (Tac2expr.raw_tacexpr, _, 'a) Pcoq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> scope_rule
type scope_interpretation = Tac2expr.sexpr list -> scope_rule
val register_scope : Names.Id.t -> scope_interpretation -> unit

Create a new scope with the provided name

val parse_scope : Tac2expr.sexpr -> scope_rule

Use this to interpret the subscopes for interpretation functions

Inspecting
val print_ltac : Libnames.qualid -> unit
Eval loop
val call : pstate:Declare.Proof.t -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t

Evaluate a tactic expression in the current environment

Toplevel exceptions
val backtrace : Tac2expr.backtrace Exninfo.t
Parsing entries
module Pltac : sig ... end
Hooks
val register_constr_quotations : (unit -> unit) Hook.t