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