Tac2entries (p.rocq-runtime.9.2.0.doc.ltac2_plugin.Ltac2

Toplevel definitions

val register_ltac : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  ?mut:bool ->
  Tac2expr.rec_flag ->
  (Names.lname * Tac2expr.raw_tacexpr) list ->
  unit

Source

val register_type : 
  ?local:bool ->
  ?abstract:bool ->
  Tac2expr.rec_flag ->
  (Libnames.qualid * Tac2expr.redef_flag * Tac2expr.raw_quant_typedef) list ->
  unit

Sourceval import_type : Libnames.qualid -> Names.Id.t -> unit

Source

val register_primitive : 
  ?deprecation:Deprecation.t ->
  ?local:bool ->
  Names.lident ->
  Tac2expr.raw_typexpr ->
  Tac2expr.ml_tactic_name ->
  unit

Sourceval register_struct : Attributes.vernac_flags -> Tac2expr.strexpr -> unit

Sourcetype notation_interpretation_data

Sourcetype notation_target = Libnames.qualid option * int option

Source

val pr_register_notation : 
  Tac2expr.sexpr list ->
  notation_target ->
  Tac2expr.raw_tacexpr ->
  Pp.t

Source

val pr_register_abbreviation : 
  Names.Id.t CAst.t ->
  Tac2expr.raw_tacexpr ->
  Pp.t

Source

val register_notation : 
  Attributes.vernac_flags ->
  Tac2expr.sexpr list ->
  notation_target ->
  Tac2expr.raw_tacexpr ->
  notation_interpretation_data

Source

val register_abbreviation : 
  Attributes.vernac_flags ->
  Names.Id.t CAst.t ->
  Tac2expr.raw_tacexpr ->
  notation_interpretation_data

Sourceval register_notation_interpretation : notation_interpretation_data -> unit

Sourceval register_custom_entry : Names.lident -> unit

Source

val perform_eval : 
  pstate:Declare.Proof.t option ->
  Tac2expr.raw_tacexpr ->
  unit

Notations

Sourcetype syntax_class_rule =

| SyntaxRule : (Tac2expr.raw_tacexpr, _, 'a) Procq.Symbol.t * ('a -> Tac2expr.raw_tacexpr) -> syntax_class_rule

Sourcetype used_levels

Sourceval no_used_levels : used_levels

Sourceval union_used_levels : used_levels -> used_levels -> used_levels

Sourcetype 'glb syntax_class_decl = {

intern_synclass : Tac2expr.sexpr list -> used_levels * 'glb;
interp_synclass : 'glb -> syntax_class_rule;

}

Sourceval register_syntax_class : Names.Id.t -> _ syntax_class_decl -> unit

Create a new syntax class with the provided name

Sourcetype syntax_class

Sourceval intern_syntax_class : Tac2expr.sexpr -> used_levels * syntax_class

Use this to internalize the syntax class arguments for interpretation functions

Sourceval interp_syntax_class : syntax_class -> syntax_class_rule

Use this to interpret the syntax class arguments for interpretation functions

Inspecting

Sourceval print_located_tactic : Libnames.qualid -> unit

Display the absolute name of a tactic.

Sourceval print_ltac2 : Libnames.qualid -> unit

Display the definition of a tactic.

Sourceval print_ltac2_type : Libnames.qualid -> unit

Display the definition of a type.

Sourceval print_signatures : unit -> unit

Print types of all definitions in scope.

Sourceval typecheck_expr : Tac2expr.raw_tacexpr -> unit

Sourceval globalize_expr : Tac2expr.raw_tacexpr -> unit

module Tac2Custom : module type of Names.KerName

module CustomTab : Nametab.NAMETAB with type elt = Tac2Custom.t

Common APIs on name tables.

Sourceval find_custom_entry : Tac2Custom.t -> Tac2expr.raw_tacexpr Procq.Entry.t

NB: Do not save the result of this function across summary resets, the Entry.t gets regenerated on (parsing) summary unfreeze.

Eval loop

Source

val call : 
  pstate:Declare.Proof.t ->
  Goal_select.t option ->
  with_end_tac:bool CAst.t ->
  Tac2expr.raw_tacexpr ->
  Declare.Proof.t

Evaluate a tactic expression in the current environment

Source

val call_par : 
  pstate:Declare.Proof.t ->
  Tac2expr.raw_tacexpr ->
  Declare.Proof.t

Parsing entries

Sourcemodule Pltac : sig ... end