Documents how Coq terms are represented in Elpi.
Standard library of Coq specific utilities (in the coq. namespace).
Selects which files are accumulated in an Elpi Command.
Selects which files are accumulated in an Elpi Tactic.
Extends the standard type checker for Elpi programs so that it reports errors using Coq's I/O primitives.
Implementation of Ltac's like combinators in Elpi.
Implementation of reduction in Elpi. Main entry points are whd and hd-beta.
Uses the Coq type inference and unification algorithms in order to implement
of, unify-* and evar.
An elaborator completely written in Elpi (work in progress). It implements
of, unify-* and evar.