Index of types
Index of values
Index of modules
Index of module types


AAC_coq
Interface with Coq where we define some handlers for Coq's API, and we import several definitions from Coq's standard library.
AAC_helper
Debugging functions, that can be triggered on a per-file base.
AAC_search_monad
Search monad that allows to express non-deterministic algorithms in a legible maner, or programs that solve combinatorial problems.
AAC_matcher
Standalone module containing the algorithm for matching modulo associativity and associativity and commutativity (AAC).
AAC_theory
Bindings for Coq constants that are specific to the plugin; reification and translation functions.
AAC_print
Pretty printing functions we use for the aac_instances tactic.
AAC_rewrite
Definition of the tactics, and corresponding Coq grammar entries.