Ltac2 APIs

This page documents the API of MLtac2 version 1.0.0.

Re-exports of Rocq APIs under their Ltac2 name.

Documentation on this file is adapted from the Ltac2 documentation and the reference manual.

Built-in types

type ident = Names.Id.t

type evar = Evar.t

type cast = Constr.cast_kind

type constant = Names.Constant.t

type inductive = Names.Ind.t

type constructor = Names.Construct.t

type projection = Names.Projection.t

type pattern = Pattern.constr_pattern

type constr = EConstr.t

type preterm = Ltac_pretype.closed_glob_constr

type binder = Names.Name.t EConstr.binder_annot * EConstr.types

type message = Pp.t

type reference = Names.GlobRef.t

type err = Exninfo.iexn

type iexn = Exninfo.iexn

type exninfo = Exninfo.info

Ltac2 APIs

Constants

module Constant : sig ... end

Terms

module Constr : sig ... end

Constructor

module Constructor : sig ... end

Control

module Control : sig ... end

Environment

module Env : sig ... end

Fresh name generation

module Fresh : sig ... end

Identifiers

module Ident : sig ... end

Inductives

module Ind : sig ... end

Message

module Message : sig ... end

Module

module Module : sig ... end

Pattern

module Pattern : sig ... end

Projections

module Proj : sig ... end

Rewriting

module Rewrite : sig ... end

Schemes

module Scheme : sig ... end

Syntax DSL

module Syntax : sig ... end

Standard tactics

module Std : sig ... end

Transparent state

module TransparentState : sig ... end

Unification

module Unification : sig ... end