Module Ltac2_plugin.Tac2env
Toplevel definition of values
type global_data
=
{
gdata_expr : Tac2expr.glb_tacexpr;
gdata_type : Tac2expr.type_scheme;
gdata_mutable : bool;
}
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
andSome
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
val define_alias : Tac2expr.ltac_constant -> Tac2expr.raw_tacexpr -> unit
val interp_alias : Tac2expr.ltac_constant -> Tac2expr.raw_tacexpr
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 mem_constructor : Libnames.qualid -> bool
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 -> '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_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