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.

Ltac profiling primitives

Ltac profiling entrypoints

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.