Tac2env (coq-core.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

type compile_info = {

source : string;

}

val set_compiled_global : 
  Tac2expr.ltac_constant ->
  compile_info ->
  Tac2ffi.valexpr ->
  unit

val get_compiled_global : 
  Tac2expr.ltac_constant ->
  (compile_info * Tac2ffi.valexpr) option

val globals : unit -> global_data Names.KNmap.t

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

Toplevel definition of notations

val define_notation : Tac2expr.ltac_notation -> Tac2expr.raw_tacexpr -> unit

val interp_notation : Tac2expr.ltac_notation -> 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 path_of_ltac : Tac2expr.tacref -> Libnames.full_path

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 path_of_constructor : Tac2expr.ltac_constructor -> Libnames.full_path

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

This state is not part of the summary, contrarily to the ones above. It is intended to be used from ML plugins to register ML-side functions.

val define_primitive : Tac2expr.ml_tactic_name -> Tac2ffi.valexpr -> unit

val interp_primitive : Tac2expr.ml_tactic_name -> Tac2ffi.valexpr

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_ltac2in1 : 
  ( 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_ltac2in1_val : 
  ( Names.Id.t CAst.t list * Tac2expr.raw_tacexpr,
    Tac2expr.glb_tacexpr,
    Util.Empty.t )
    Genarg.genarg_type

Ltac2 quotations in Ltac1 returning Ltac1 values. When ids are bound interning turns them into Ltac1.lambda.

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

type var_quotation_kind =

| ConstrVar

| PretermVar

val wit_ltac2_var_quotation : 
  ( Names.lident option * Names.lident,
    var_quotation_kind * Names.Id.t,
    Util.Empty.t )
    Genarg.genarg_type

Ltac2 quotations for variables "$x" or "$kind:foo" in Gallina terms. NB: "$x" means "$constr:x"

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.

Helper functions

val is_constructor_id : Names.Id.t -> bool

val is_constructor : Libnames.qualid -> bool