package rocq-runtime

  1. Overview
  2. Docs

Module Ltac2_plugin.Tac2entriesSource

Toplevel definitions
Sourceval register_ltac : ?deprecation:Deprecation.t -> ?local:bool -> ?mut:bool -> Tac2expr.rec_flag -> (Names.lname * Tac2expr.raw_tacexpr) list -> unit
Sourceval 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
Sourceval register_primitive : ?deprecation:Deprecation.t -> ?local:bool -> Names.lident -> Tac2expr.raw_typexpr -> Tac2expr.ml_tactic_name -> unit
Sourcetype ('scope, 'body) notation_interpretation_data
Sourceval pr_register_abbreviation : Names.Id.t CAst.t -> Tac2expr.raw_tacexpr -> Pp.t
Sourceval register_abbreviation : Attributes.vernac_flags -> Names.Id.t CAst.t -> 'body -> (_ option, 'body) notation_interpretation_data
Sourceval register_notation_interpretation : (Libnames.qualid option, Tac2expr.raw_tacexpr) notation_interpretation_data -> unit
Sourceval register_struct : Attributes.vernac_flags -> Tac2expr.strexpr -> unit
Sourceval perform_eval : pstate:Declare.Proof.t option -> Tac2expr.raw_tacexpr -> unit
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
Eval loop
Sourceval 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

Parsing entries
Sourcemodule Pltac : sig ... end