package coq-core

  1. Overview
  2. Docs
On This Page
  1. Hardwired data
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type
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 =
  1. | Any : (_, _, _) map_tag -> any_map_tag
type tagged_set =
  1. | TaggedSet : (_, 'set, _) map_tag * 'set -> tagged_set
type tagged_map =
  1. | 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
OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events Blog Jobs
Resources
Install OCaml Get Started Platform Tools Language Manual Standard Library API Books Exercises Papers OCaml Playground Logo
Policies
Carbon Footprint Governance Privacy Code of Conduct