Module Ltac2_plugin.Tac2entries

Toplevel definitions
val register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> Tac2expr.rec_flag -> (Names.lname * Tac2expr.raw_tacexpr) list -> unit
val register_type : ?local:bool -> ?abstract:bool -> Tac2expr.rec_flag -> (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list -> unit
val register_primitive : ?deprecation:Deprecation.t -> ?local:bool -> Names.lident -> Tac2expr.raw_typexpr -> Tac2expr.ml_tactic_name -> unit
val register_struct : Attributes.vernac_flags -> Tac2expr.strexpr -> unit
type notation_interpretation_data
val pr_register_notation : Tac2expr.sexpr list -> int option -> Tac2expr.raw_tacexpr -> Pp.t
val register_notation_interpretation : notation_interpretation_data -> unit
val perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
Notations
type syntax_class_rule =
| SyntaxRule : (Tac2expr.raw_tacexpr, _, 'a) Procq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> syntax_class_rule
type syntax_class_interpretation = Tac2expr.sexpr list -> syntax_class_rule
val register_syntax_class : Names.Id.t -> syntax_class_interpretation -> unit

Create a new syntax class with the provided name

val parse_syntax_class : Tac2expr.sexpr -> syntax_class_rule

Use this to interpret the syntax class arguments for interpretation functions

Inspecting
val print_located_tactic : Libnames.qualid -> unit

Display the absolute name of a tactic.

val print_ltac2 : Libnames.qualid -> unit

Display the definition of a tactic.

val print_ltac2_type : Libnames.qualid -> unit

Display the definition of a type.

val print_signatures : unit -> unit

Print types of all definitions in scope.

val typecheck_expr : Tac2expr.raw_tacexpr -> unit
val globalize_expr : Tac2expr.raw_tacexpr -> unit
Eval loop
val call : pstate:Declare.Proof.t -> Goal_select.t option -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t

Evaluate a tactic expression in the current environment

val call_par : pstate:Declare.Proof.t -> with_end_tac:bool -> Tac2expr.raw_tacexpr -> Declare.Proof.t
Parsing entries
module Pltac : sig ... end