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.

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

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

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).