| 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. |
| Search_monad | Search monad that allows to express non-deterministic algorithms in a legible maner, or programs that solve combinatorial problems. |
| Matcher | Standalone module containing the algorithm for matching modulo associativity and associativity and commutativity (AAC). |
| Theory | Bindings for Coq constants that are specific to the plugin; reification and translation functions. |
Pretty printing functions we use for the aac_instances tactic. | |
| Aac_rewrite | aac_rewrite -- rewriting modulo A or AC |