Index of modules

A
Aac_rewrite

aac_rewrite -- rewriting modulo A or AC

C
Classes [Coq]

Coq typeclasses

Coq

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

D
Debug [Helper]
E
Equivalence [Coq]
H
Helper

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

L
List [Coq]

Coq lists

M
Matcher

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

N
Nat [Coq]

Coq unary numbers (peano)

O
Option [Coq]
P
Pair [Coq]

Coq pairs

Pos [Coq]

Coq positive numbers (pos)

Print

Pretty printing functions we use for the aac_instances tactic.

R
Relation [Coq]
Rewrite [Coq]
S
Search_monad

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

Sigma [Theory]

Environments

Stubs [Theory]

We need to export some Coq stubs out of this module.

Subst [Matcher]

Substitutions (or environments)

Sym [Theory]

Dynamically typed morphisms

T
Terms [Matcher]

Representations of expressions

Theory

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

Trans [Theory]

Tranlations between Coq and OCaml