package coq-core

  1. Overview
  2. Docs
On This Page
  1. Hardwired data
package coq-core
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Ltac2_plugin.Tac2coreSource

Hardwired data
Sourcemodule Core : sig ... end
Sourceval throw : ?info:Exninfo.info -> exn -> 'a Proofview.tactic
Sourceval pf_apply : ?catch_exceptions:bool -> (Environ.env -> Evd.evar_map -> 'a Proofview.tactic) -> 'a Proofview.tactic
Sourcemodule type MapType = sig ... end
Sourcetype ('a, 'set, 'map) map_tag
Sourcetype any_map_tag =
  1. | Any : (_, _, _) map_tag -> any_map_tag
Sourcetype tagged_set =
  1. | TaggedSet : (_, 'set, _) map_tag * 'set -> tagged_set
Sourcetype tagged_map =
  1. | TaggedMap : (_, _, 'map) map_tag * 'map -> tagged_map
Sourceval map_tag_repr : any_map_tag Tac2ffi.repr
Sourceval 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

OCaml

Innovation. Community. Security.

GitHub Discord Twitter Peertube RSS
About
Changelog Releases Industrial Users Academic Users Why OCaml
Ecosystem
Packages Community Events OCaml Planet 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