package rocq-runtime

You can search for identifiers within the package.

in-package search v0.2.0

The Rocq Prover -- Core Binaries and Tools

Install

Dune Dependency

rocq-prover.org Readme Edit opam file Versions (1)

Authors

T

The Rocq development team, INRIA, CNRS, and contributors

Maintainers

T

The Rocq development team <coqdev@inria.fr>

Sources

rocq-9.0.0.tar.gz

md5=8d522602d23e7a665631826dab9aa92b

sha512=f4f76a6a178e421c99ee7a331a2fd97a06e9c5d0168d7e60c44e3820d8e1a124370ea104ad90c7f87a9a1e9d87b2d0d7d2d387c998feeaed4a75ed04e176a4be

doc/ltac2_plugin/Ltac2_plugin/Tac2core/index.html

Module `Ltac2_plugin.Tac2core`Source

Hardwired data

Sourcemodule Core : sig ... end

Sourceval throw : ?info:Exninfo.info -> exn -> 'a Proofview.tactic

Source

val 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 =

| Any : (_, _, _) map_tag -> any_map_tag

Sourcetype tagged_set =

| TaggedSet : (_, 'set, _) map_tag * 'set -> tagged_set

Sourcetype tagged_map =

| TaggedMap : (_, _, 'map) map_tag * 'map -> tagged_map

Sourceval map_tag_repr : any_map_tag Tac2ffi.repr

Sourceval set_repr : tagged_set Tac2ffi.repr

Sourceval map_repr : tagged_map Tac2ffi.repr

Source

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

Source

val ident_map_tag : 
  (Names.Id.t, Names.Id.Set.t, Tac2val.valexpr Names.Id.Map.t) map_tag

Sourceval int_map_tag : (int, Int.Set.t, Tac2val.valexpr Int.Map.t) map_tag

Source

val string_map_tag : 
  (string, CString.Set.t, Tac2val.valexpr CString.Map.t) map_tag

Source

val inductive_map_tag : 
  (Names.inductive, Names.Indset_env.t, Tac2val.valexpr Names.Indmap_env.t)
    map_tag

Source

val constructor_map_tag : 
  (Names.constructor,
    Names.Constrset_env.t,
    Tac2val.valexpr Names.Constrmap_env.t)
    map_tag

Source

val constant_map_tag : 
  (Names.Constant.t, Names.Cset_env.t, Tac2val.valexpr Names.Cmap_env.t)
    map_tag

On This Page

Hardwired data

package rocq-runtime

Install

Dune Dependency

Authors

Maintainers

Sources

doc/ltac2_plugin/Ltac2_plugin/Tac2core/index.html

Module Ltac2_plugin.Tac2coreSource

Hardwired data

Module `Ltac2_plugin.Tac2core`Source