Aac_rewrite
Definition of the tactics, and corresponding Coq grammar entries.
Coq
Interface with Coq where we define some handlers for Coq's API, and we import several definitions from Coq's standard library.
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.