Coq
Interface with Coq where we define some handlers for Coq's API, and we import several definitions from Coq's standard library.
Evm_compute
evm_compute eq blacklist performs a vm_compute step with the following provisos: evars can appear in the goal; terms that are equal (modulo eq) to terms in the blacklist are abstracted before-hand.
Helper
Debugging functions, that can be triggered on a per-file base.
Matcher
Standalone module containing the algorithm for matching modulo associativity and associativity and commutativity (AAC).
Print
Pretty printing functions we use for the aac_instances tactic.
Search_monad
Search monad that allows to express non-deterministic algorithms in a legible maner, or programs that solve combinatorial problems.
Theory
Bindings for Coq constants that are specific to the plugin; reification and translation functions.