package coq-core

  1. Overview
  2. Docs
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.