Tac2core (coq-core.Ltac2_plugin.Tac2core)

Hardwired data

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.

Default registered maps

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