Module `Ltac2_plugin.Tac2env`Source

Ltac2 global environment

Toplevel definition of values

Sourcetype global_data = {

gdata_expr : Tac2expr.glb_tacexpr;
gdata_type : Tac2expr.type_scheme;
gdata_mutable : bool;
gdata_deprecation : Deprecation.t option;

}

Sourceval define_global : Tac2expr.ltac_constant -> global_data -> unit

Sourceval interp_global : Tac2expr.ltac_constant -> global_data

Sourcetype compile_info = {

source : string;

}

Source

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

Source

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

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

Toplevel definition of types

Sourceval define_type : Tac2expr.type_constant -> Tac2expr.glb_quant_typedef -> unit

Sourceval interp_type : Tac2expr.type_constant -> Tac2expr.glb_quant_typedef

Toplevel definition of algebraic constructors

Sourcetype 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.
*)

}

Source

val define_constructor : 
  ?warn:UserWarn.t ->
  Tac2expr.ltac_constructor ->
  constructor_data ->
  unit

Sourceval interp_constructor : Tac2expr.ltac_constructor -> constructor_data

Source

val find_all_constructors_in_type : 
  Tac2expr.type_constant ->
  constructor_data Names.KNmap.t

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

Toplevel definition of projections

Sourcetype 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
*)

}

Sourceval define_projection : Tac2expr.ltac_projection -> projection_data -> unit

Sourceval interp_projection : Tac2expr.ltac_projection -> projection_data

Toplevel definition of aliases

Sourcetype alias_data = {

alias_body : Tac2expr.raw_tacexpr;
alias_depr : Deprecation.t option;

}

Source

val define_alias : 
  ?deprecation:Deprecation.t ->
  Tac2expr.ltac_constant ->
  Tac2expr.raw_tacexpr ->
  unit

Sourceval interp_alias : Tac2expr.ltac_constant -> alias_data

Toplevel definition of notations

Sourcetype notation_data =

| UntypedNota of Tac2expr.raw_tacexpr
| TypedNota of {
1. nota_prms : int;
2. nota_argtys : int Tac2expr.glb_typexpr Names.Id.Map.t;
3. nota_ty : int Tac2expr.glb_typexpr;
4. nota_body : Tac2expr.glb_tacexpr;
}

Sourceval define_notation : Tac2expr.ltac_notation -> notation_data -> unit

Sourceval interp_notation : Tac2expr.ltac_notation -> notation_data

Name management

Source

val push_ltac : 
  Nametab.visibility ->
  Libnames.full_path ->
  Tac2expr.tacref ->
  unit

Sourceval locate_ltac : Libnames.qualid -> Tac2expr.tacref

Sourceval locate_extended_all_ltac : Libnames.qualid -> Tac2expr.tacref list

Source

val shortest_qualid_of_ltac : 
  Names.Id.Set.t ->
  Tac2expr.tacref ->
  Libnames.qualid

Sourceval path_of_ltac : Tac2expr.tacref -> Libnames.full_path

Source

val push_constructor : 
  Nametab.visibility ->
  Libnames.full_path ->
  Tac2expr.ltac_constructor ->
  unit

Sourceval locate_constructor : Libnames.qualid -> Tac2expr.ltac_constructor

Source

val locate_extended_all_constructor : 
  Libnames.qualid ->
  Tac2expr.ltac_constructor list

Source

val shortest_qualid_of_constructor : 
  Tac2expr.ltac_constructor ->
  Libnames.qualid

Sourceval path_of_constructor : Tac2expr.ltac_constructor -> Libnames.full_path

Sourceval constructor_user_warn : ?loc:Loc.t -> Tac2expr.ltac_constructor -> unit

Emit warning if any for the constructor.

Source

val push_type : 
  Nametab.visibility ->
  Libnames.full_path ->
  Tac2expr.type_constant ->
  unit

Sourceval locate_type : Libnames.qualid -> Tac2expr.type_constant

Sourceval locate_extended_all_type : Libnames.qualid -> Tac2expr.type_constant list

Source

val shortest_qualid_of_type : 
  ?loc:Loc.t ->
  Tac2expr.type_constant ->
  Libnames.qualid

Sourceval path_of_type : Tac2expr.type_constant -> Libnames.full_path

Source

val push_projection : 
  Nametab.visibility ->
  Libnames.full_path ->
  Tac2expr.ltac_projection ->
  unit

Sourceval locate_projection : Libnames.qualid -> Tac2expr.ltac_projection

Source

val locate_extended_all_projection : 
  Libnames.qualid ->
  Tac2expr.ltac_projection list

Sourceval 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.

Sourceval define_primitive : Tac2expr.ml_tactic_name -> Tac2val.valexpr -> unit

Sourceval interp_primitive : Tac2expr.ml_tactic_name -> Tac2val.valexpr

ML primitive types

Sourcetype 'a or_glb_tacexpr =

| GlbVal of 'a
| GlbTacexpr of Tac2expr.glb_tacexpr

Source

type ('a, 'b, 'r) intern_fun =
  Genintern.glob_sign ->
  'a ->
  'b * 'r Tac2expr.glb_typexpr

Sourcetype environment = {

env_ist : Tac2val.valexpr Names.Id.Map.t;

}

Sourcetype ('a, 'b) ml_object = {

ml_intern : 'r. ('a, 'b or_glb_tacexpr, 'r) intern_fun;
ml_subst : Mod_subst.substitution -> 'b -> 'b;
ml_interp : environment -> 'b -> Tac2val.valexpr Proofview.tactic;
ml_print : Environ.env -> Evd.evar_map -> 'b -> Pp.t;
ml_raw_print : Environ.env -> Evd.evar_map -> 'a -> Pp.t;

}

Sourceval define_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object -> unit

Sourceval interp_ml_object : ('a, 'b) Tac2dyn.Arg.tag -> ('a, 'b) ml_object

Absolute paths

Sourceval rocq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

Sourceval coq_prefix : Names.ModPath.t

Path where primitive datatypes are defined in Ltac2 plugin.

deprecated (9.0) Use rocq_prefix

Sourceval std_prefix : Names.ModPath.t

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

Sourceval ltac1_prefix : Names.ModPath.t

Path where the Ltac1 legacy FFI is defined.

Generic arguments

Source

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

Sourcetype var_quotation_kind =

| ConstrVar
| PretermVar
| PatternVar

Source

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"

Helper functions

Sourceval is_constructor_id : Names.Id.t -> bool

Sourceval is_constructor : Libnames.qualid -> bool

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2env/index.html

Module `Ltac2_plugin.Tac2env`Source

Toplevel definition of values

Toplevel definition of types

Toplevel definition of algebraic constructors

Toplevel definition of projections

Toplevel definition of aliases

Toplevel definition of notations

Name management

Toplevel definitions of ML tactics

ML primitive types

Absolute paths

Generic arguments

Helper functions

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2env/index.html

Module Ltac2_plugin.Tac2envSource

Toplevel definition of values

Toplevel definition of types

Toplevel definition of algebraic constructors

Toplevel definition of projections

Toplevel definition of aliases

Toplevel definition of notations

Name management

Toplevel definitions of ML tactics

ML primitive types

Absolute paths

Generic arguments

Helper functions

Module `Ltac2_plugin.Tac2env`Source