Module Ltac2_plugin.Tac2env

Toplevel definition of values
type global_data = {
gdata_expr : Tac2expr.glb_tacexpr;
gdata_type : Tac2expr.type_scheme;
gdata_mutable : bool;
gdata_deprecation : Deprecation.t option;
}
val define_global : Tac2expr.ltac_constant -> global_data -> unit
val interp_global : Tac2expr.ltac_constant -> global_data
Toplevel definition of types
val define_type : Tac2expr.type_constant -> Tac2expr.glb_quant_typedef -> unit
val interp_type : Tac2expr.type_constant -> Tac2expr.glb_quant_typedef
Toplevel definition of algebraic constructors
type constructor_data = {
cdata_prms : int;

Type parameters

cdata_type : Tac2expr.type_constant;

Inductive definition to which the constructor pertains

cdata_args : int Tac2expr.glb_typexpr list;

Types of the constructor arguments

cdata_indx : int option;

Index of the constructor in the ADT. Numbering is duplicated between argumentless and argument-using constructors, e.g. in type 'a option None and Some have both index 0. This field is empty whenever the constructor is a member of an open type.

}
val define_constructor : Tac2expr.ltac_constructor -> constructor_data -> unit
val interp_constructor : Tac2expr.ltac_constructor -> constructor_data
Toplevel definition of projections
type projection_data = {
pdata_prms : int;

Type parameters

pdata_type : Tac2expr.type_constant;

Record definition to which the projection pertains

pdata_ptyp : int Tac2expr.glb_typexpr;

Type of the projection

pdata_mutb : bool;

Whether the field is mutable

pdata_indx : int;

Index of the projection

}
val define_projection : Tac2expr.ltac_projection -> projection_data -> unit
val interp_projection : Tac2expr.ltac_projection -> projection_data
Toplevel definition of aliases
type alias_data = {
alias_body : Tac2expr.raw_tacexpr;
alias_depr : Deprecation.t option;
}
val define_alias : ?⁠deprecation:Deprecation.t -> Tac2expr.ltac_constant -> Tac2expr.raw_tacexpr -> unit
val interp_alias : Tac2expr.ltac_constant -> alias_data
Name management
val push_ltac : Nametab.visibility -> Libnames.full_path -> Tac2expr.tacref -> unit
val locate_ltac : Libnames.qualid -> Tac2expr.tacref
val locate_extended_all_ltac : Libnames.qualid -> Tac2expr.tacref list
val shortest_qualid_of_ltac : Tac2expr.tacref -> Libnames.qualid
val push_constructor : Nametab.visibility -> Libnames.full_path -> Tac2expr.ltac_constructor -> unit
val locate_constructor : Libnames.qualid -> Tac2expr.ltac_constructor
val locate_extended_all_constructor : Libnames.qualid -> Tac2expr.ltac_constructor list
val shortest_qualid_of_constructor : Tac2expr.ltac_constructor -> Libnames.qualid
val push_type : Nametab.visibility -> Libnames.full_path -> Tac2expr.type_constant -> unit
val locate_type : Libnames.qualid -> Tac2expr.type_constant
val locate_extended_all_type : Libnames.qualid -> Tac2expr.type_constant list
val shortest_qualid_of_type : ?⁠loc:Loc.t -> Tac2expr.type_constant -> Libnames.qualid
val push_projection : Nametab.visibility -> Libnames.full_path -> Tac2expr.ltac_projection -> unit
val locate_projection : Libnames.qualid -> Tac2expr.ltac_projection
val locate_extended_all_projection : Libnames.qualid -> Tac2expr.ltac_projection list
val shortest_qualid_of_projection : Tac2expr.ltac_projection -> Libnames.qualid
Toplevel definitions of ML tactics
val define_primitive : Tac2expr.ml_tactic_name -> Tac2ffi.closure -> unit
val interp_primitive : Tac2expr.ml_tactic_name -> Tac2ffi.closure
ML primitive types
type 'a or_glb_tacexpr =
| GlbVal of 'a
| GlbTacexpr of Tac2expr.glb_tacexpr
type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r Tac2expr.glb_typexpr
type environment = {
env_ist : Tac2ffi.valexpr Names.Id.Map.t;
}
type ('a, 'b) ml_object = {
ml_intern : r. (Tac2expr.raw_tacexpr, Tac2expr.glb_tacexpr, 'r) intern_fun -> ('a, 'b or_glb_tacexpr, 'r) intern_fun;
ml_subst : Mod_subst.substitution -> 'b -> 'b;
ml_interp : environment -> 'b -> Tac2ffi.valexpr Proofview.tactic;
ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
}
val define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit
val interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object
Absolute paths
val coq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

val std_prefix : Names.ModPath.t

Path where Ltac-specific datatypes are defined in Ltac2 plugin.

val ltac1_prefix : Names.ModPath.t

Path where the Ltac1 legacy FFI is defined.

Generic arguments
val wit_ltac2 : (Names.Id.t CAst.t list * Tac2expr.raw_tacexpr, Names.Id.t list * Tac2expr.glb_tacexpr, Util.Empty.t) Genarg.genarg_type

Ltac2 quotations in Ltac1 code

val wit_ltac2_val : (Util.Empty.t, unit, Util.Empty.t) Genarg.genarg_type

Embedding Ltac2 closures of type Ltac1.t -> Ltac1.t inside Ltac1. There is no relevant data because arguments are passed by conventional names.

val wit_ltac2_constr : (Tac2expr.raw_tacexpr, Names.Id.Set.t * Tac2expr.glb_tacexpr, Util.Empty.t) Genarg.genarg_type

Ltac2 quotations in Gallina terms

val wit_ltac2_quotation : (Names.Id.t Loc.located, Names.Id.t, Util.Empty.t) Genarg.genarg_type

Ltac2 quotations for variables "$x" in Gallina terms

Helper functions
val is_constructor_id : Names.Id.t -> bool
val is_constructor : Libnames.qualid -> bool