Interface with Coq where we define some handlers for Coq's API, and we import several definitions from Coq's standard library.

Debugging functions, that can be triggered on a per-file base.

Search monad that allows to express non-deterministic algorithms in a legible maner, or programs that solve combinatorial problems.

Standalone module containing the algorithm for matching modulo associativity and associativity and commutativity (AAC).

Bindings for Coq constants that are specific to the plugin; reification and translation functions.

Pretty printing functions we use for the aac_instances tactic.