package coq-core

  1. Overview
  2. Docs
package coq-core
Legend:
Library
Module
Module type
Parameter
Class
Class type

Interface for defining external tactics via a high-level spec.

type (_, _) spec

Type ('v,'f) spec represents a high-level Ltac2 tactic specification. It indicates how to turn a value of type 'f into an Ltac2 tactic, which may involve converting between OCaml and Ltac2 value representations, and also lifting a pure function to the tactic monad. The type parameter 'v gives the type of value produced by interpreting the specification.

tac r is the specification of a tactic (in the tactic monad sense) whose return type is specified (and converted into an Ltac2 value) via r.

tac' is similar to tac, but only needs a conversion function.

ret r is the specification of a pure tactic (i.e., a tactic defined as a pure OCaml value, not needing the tactic monad) whose return type is given by r (see tac).

ret' is similar to ret, but only needs a conversion function.

eret is similar to ret, but for tactics that can be implemented with a pure OCaml value, provided extra arguments env and sigma, computed via tclENV and tclEVARMAP.

eret' is similar to eret, but only needs a conversion function.

gret is similar to ret, but for tactics that can be implemented with a pure OCaml value, provided the current goal g as extra argument. A fatal error is produced when there is not exactly one goal in focus at the point of using an Ltac2 value defined with this specification. Indeed, the value of g is computed using Goal.enter_one.

gret' is similar to gret, but only needs a conversion function.

val (@->) : 'a Tac2ffi.repr -> ('t, 'f) spec -> (Tac2ffi.valexpr -> 't, 'a -> 'f) spec

r @-> s extends the specification s with a closure argument whose type is specified by (and converted from an Ltac2 value via) r.

val (@-->) : (Tac2ffi.valexpr -> 'a) -> ('t, 'f) spec -> (Tac2ffi.valexpr -> 't, 'a -> 'f) spec

(@-->) is similar to (@->), but only needs a conversion function.

val define : Tac2expr.ml_tactic_name -> (_, 'f) spec -> 'f -> unit

define tac s f defines an external tactic tac by interpreting f with the specification s. The Invalid_argument exception is raised when the given s does not produce a "pure" tactic, that is, something that can be turned into an Ltac2 value (i.e., a closure, or a pure value).

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