Module `Ltac2_plugin.Tac2core`

module Core : sig ... end

val throw : ?⁠info:Exninfo.info -> exn -> 'a Proofview.tactic
val pf_apply : ?⁠catch_exceptions:bool -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic

module type MapType = sig ... end

type ('a, 'set, 'map) map_tag
type any_map_tag = | Any : (_, _, _) map_tag -> any_map_tag
type tagged_set = | TaggedSet : (_, 'set, _) map_tag * 'set -> tagged_set
type tagged_map = | TaggedMap : (_, _, 'map) map_tag * 'map -> tagged_map

val map_tag_repr : any_map_tag Tac2ffi.repr
val set_repr : tagged_set Tac2ffi.repr
val map_repr : tagged_map Tac2ffi.repr
val register_map : ?⁠plugin:string -> tag_name:string -> (module MapType with type valmap = 'map and type S.elt = 'a and type S.t = 'set) -> ('a, 'set, 'map) map_tag: Register a type on which we can use finite sets and maps. tag_name is the name used for the external to make the Ltac2.FSet.Tags.tag available.

val ident_map_tag : (Names.Id.t, Names.Id.Set.t, Tac2ffi.valexpr Names.Id.Map.t) map_tag
val int_map_tag : (int, Int.Set.t, Tac2ffi.valexpr Int.Map.t) map_tag
val string_map_tag : (string, CString.Set.t, Tac2ffi.valexpr CString.Map.t) map_tag
val inductive_map_tag : (Names.inductive, Names.Indset_env.t, Tac2ffi.valexpr Names.Indmap_env.t) map_tag
val constructor_map_tag : (Names.constructor, Names.Constrset_env.t, Tac2ffi.valexpr Names.Constrmap_env.t) map_tag
val constant_map_tag : (Names.Constant.t, Names.Cset_env.t, Tac2ffi.valexpr Names.Cmap_env.t) map_tag