This module defines potentially focussing tactics. They are used by Ltac to emulate the historical behaviour of always-focussed tactics while still allowing to remain global when the goal is not needed.

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

Ltac parsing entries

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

Tactic related witnesses, could also live in tactics/ if other users

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.

Ltac toplevel command entries.

This module centralizes the various ways of registering tactics.

Globalization of tactic expressions : Conversion from raw_tactic_expr to glob_tactic_expr

Substitution of tactics at module closing time

TODO: Move those definitions somewhere sensible

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