Module Ltac2_plugin.Tac2env

Ltac2 global environment

Toplevel definition of values
type global_data = {
  1. gdata_expr : Tac2expr.glb_tacexpr;
  2. gdata_type : Tac2expr.type_scheme;
  3. gdata_mutable : bool;
  4. gdata_deprecation : Deprecation.t option;
  5. gdata_mutation_history : Names.ModPath.t list;
}
val define_global : Tac2expr.ltac_constant -> global_data -> unit
val interp_global : Tac2expr.ltac_constant -> global_data
type compile_info = {
  1. source : string;
}
val set_compiled_global : Tac2expr.ltac_constant -> compile_info -> Tac2val.valexpr -> unit
val get_compiled_global : Tac2expr.ltac_constant -> (compile_info * Tac2val.valexpr) option
val globals : unit -> global_data Names.KerName.Map.t
Toplevel definition of types
Toplevel definition of algebraic constructors
type constructor_data = {
  1. cdata_prms : int;
    (*

    Type parameters

    *)
  2. cdata_type : Tac2expr.type_constant;
    (*

    Inductive definition to which the constructor pertains

    *)
  3. cdata_args : int Tac2expr.glb_typexpr list;
    (*

    Types of the constructor arguments

    *)
  4. 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
val find_all_constructors_in_type : Tac2expr.type_constant -> constructor_data Names.KerName.Map.t

Useful for printing info about currently defined constructors of open types.

Toplevel definition of projections
type projection_data = {
  1. pdata_prms : int;
    (*

    Type parameters

    *)
  2. pdata_type : Tac2expr.type_constant;
    (*

    Record definition to which the projection pertains

    *)
  3. pdata_ptyp : int Tac2expr.glb_typexpr;
    (*

    Type of the projection

    *)
  4. pdata_mutb : bool;
    (*

    Whether the field is mutable

    *)
  5. 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 abbreviations
type abbrev_data = {
  1. abbrev_prms : int;
  2. abbrev_ty : int Tac2expr.glb_typexpr;
  3. abbrev_body : Tac2expr.glb_tacexpr;
  4. abbrev_depr : Deprecation.t option;
}
val define_abbrev : Tac2expr.ltac_constant -> abbrev_data -> unit
val interp_abbrev : Tac2expr.ltac_constant -> abbrev_data
Name management
val locate_ltac : Libnames.qualid -> Tac2expr.tacref
val locate_extended_all_ltac : Libnames.qualid -> Tac2expr.tacref list
val shortest_qualid_of_ltac : ?loc:Loc.t -> ?force_short:bool -> Names.Id.Set.t -> Tac2expr.tacref -> Libnames.qualid
val path_of_ltac : Tac2expr.tacref -> Libnames.full_path
val push_constructor : ?user_warns:UserWarn.t -> 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 locate_extended_all_type : Libnames.qualid -> Tac2expr.type_constant list
val shortest_qualid_of_type : ?loc:Loc.t -> Tac2expr.type_constant -> Libnames.qualid
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 -> Tac2val.valexpr -> unit
val interp_primitive : Tac2expr.ml_tactic_name -> Tac2val.valexpr
ML primitive types
type 'a or_glb_tacexpr =
  1. | GlbVal of 'a
  2. | GlbTacexpr of Tac2expr.glb_tacexpr
type ('a, 'b, 'r) intern_fun = Genintern.glob_sign -> 'a -> 'b * 'r Tac2expr.glb_typexpr
type environment = {
  1. env_ist : Tac2val.valexpr Names.Id.Map.t;
}
type ('a, 'b) ml_object = {
  1. ml_intern : 'r. ('a, 'b or_glb_tacexpr, 'r) intern_fun;
  2. ml_subst : Mod_subst.substitution -> 'b -> 'b;
  3. ml_interp : environment -> 'b -> Tac2val.valexpr Proofview.tactic;
  4. ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
  5. ml_raw_print : Environ.env -> Evd.evar_map -> 'a -> 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 rocq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

val coq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

  • deprecated (9.0) Use rocq_prefix
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

Ltac2 quotations in Gallina terms

Ltac2 as a generic tactic depending on proof mode (eg as argument to Solve Obligations)

type var_quotation_kind =
  1. | ConstrVar
  2. | PretermVar
  3. | PatternVar
  4. | HypVar
val wit_ltac2_var_quotation : (Names.lident option * Names.lident, var_quotation_kind * Names.Id.t) GenConstr.tag

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

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