Index of modules


B
Bool [Coq]

C
Classes [Coq]
Coq typeclasses
Comparison [Coq]
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]
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.

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

L
Leibniz [Coq]
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
Transitive [Coq]