Module Ltac_plugin

module ComRewrite : sig ... end
module Coretactics : sig ... end
module Extraargs : sig ... end
module Extratactics : sig ... end
module G_auto : sig ... end
module G_class : sig ... end
module G_eqdecide : sig ... end
module G_ltac : sig ... end
module G_obligations : sig ... end
module G_rewrite : sig ... end
module G_tactic : sig ... end
module Internals : sig ... end

Implementation of Ltac-specific code to be exported in mlg files.

module Leminv : sig ... end
module Pltac : sig ... end

Ltac parsing entries

module Pptactic : sig ... end

This module implements pretty-printers for ltac_expr syntactic objects and their subcomponents.

module Profile_ltac : sig ... end

Ltac profiling primitives

module Profile_ltac_tactics : sig ... end

Ltac profiling entrypoints

module Tacarg : sig ... end
module Taccoerce : sig ... end

Coercions from highest level generic arguments to actual data used by Ltac interpretation. Those functions examinate dynamic types and try to return something sensible according to the object content.

module Tacentries : sig ... end

Ltac toplevel command entries.

module Tacenv : sig ... end

This module centralizes the various ways of registering tactics.

module Tacexpr : sig ... end
module Tacintern : sig ... end

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

module Tacinterp : sig ... end
module Tacsubst : sig ... end

Substitution of tactics at module closing time

module Tactic_debug : sig ... end

TODO: Move those definitions somewhere sensible

module Tactic_matching : sig ... end

This file extends Matching with the main logic for Ltac's (lazy)match and (lazy)match goal.

module Tactic_option : sig ... end