Applications written in Rocq-Elpi
====================================

- `Derive
  <https://github.com/LPCIC/coq-elpi/blob/master/apps/derive/examples/usage.v>`_
  shows how to obtain proved equality tests and a few extra gadgets out of
  inductive type declarations. See the `README
  <https://github.com/LPCIC/coq-elpi/blob/master/apps/derive/README.md>`_ for
  the list of derivations. It comes bundled with Rocq-Elpi.
- `Locker <https://github.com/LPCIC/coq-elpi/tree/master/apps/locker>`_ lets
  one hide the computational contents of definitions via modules or opaque
  locks. It comes bundled with Rocq-Elpi.
- `Hierarchy Builder <https://github.com/math-comp/hierarchy-builder>`_ is a
  Rocq extension to declare hierarchies of algebraic structures.
- `Algebra Tactics <https://github.com/math-comp/algebra-tactics/>`_ is a
  port of the ``ring`` and ``field`` tactics to the Mathematical Components
  library.
- `Trakt <https://github.com/ecranceMERCE/trakt>`_ is a generic goal
  preprocessing tool for proof automation tactics in Rocq.
- `Namespace Emulation System
  <https://github.com/LPCIC/coq-elpi/blob/master/apps/NES/examples/usage_NES.v>`_
  implements most of the features of namespaces (on top of Rocq's modules).
- `Dx <https://gitlab.univ-lille.fr/samuel.hym/dx>`_ uses Elpi to generate an
  intermediate representation of Rocq terms, to be later transformed into C.
- `Coercion <https://github.com/LPCIC/coq-elpi/tree/master/apps/coercion>`_
  enables one to program coercions in Elpi. It comes bundled with Rocq-Elpi.
- `Record builder
  <https://github.com/LPCIC/coq-elpi/tree/master/apps/rbuild>`_ implements
  fancy record build/update syntax. It comes bundled with Rocq-Elpi.