Module Ltac_pluginSource

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

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

Sourcemodule Leminv : sig ... end
Sourcemodule Pltac : sig ... end

Ltac parsing entries

Sourcemodule Pptactic : sig ... end

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

Sourcemodule Profile_ltac_tactics : sig ... end
Sourcemodule Tacarg : sig ... end
Sourcemodule 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.

Sourcemodule Tacentries : sig ... end

Ltac toplevel command entries.

Sourcemodule Tacenv : sig ... end

This module centralizes the various ways of registering tactics.

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

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

Sourcemodule Tacinterp : sig ... end
Sourcemodule Tacsubst : sig ... end

Substitution of tactics at module closing time

Sourcemodule Tactic_debug : sig ... end

TODO: Move those definitions somewhere sensible

Sourcemodule Tactic_matching : sig ... end

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

Sourcemodule Tactic_option : sig ... end