ClauseQueue 
Priority Queue of clauses

Clause 
Clauses

SClause 
Simple Clause

Const 
Configuration and Globals

Extensions 
Dynamic extensions

Ctx 
Basic context for literals, clauses...

Proof 
Manipulate proofs

ProofState 
The state of a proof, contains a set of active clauses (processed),
a set of passive clauses (to be processed), and an ordering
that is used for redundancy elimination.

Saturate 
Main saturation algorithm.

Selection 
Selection functions

AC 
AC redundancy

AC_intf 
Declare that the given symbol is AC, and update the Env subsequently
by adding clauses, etc.

SimplM 
Simplification Monad

Params 
Parameters for the prover, etc.

Env 
Global environment for an instance of the prover

Signals 
Useful signals

Classify_cst 
Classification of Constants

Ctx_intf 
current ordering on terms

Clause_intf 
Flags

Env_intf 
An inference returns a list of conclusions

ProofState_intf 
Set of active clauses

BBox 
BBox (Boolean Box)

ClauseContext 
Clause context

ClauseQueue_intf 
A priority queue of clauses, purely functional

Bool_lit 
Boolean Literal

Bool_lit_intf 
Additional data carried in the literal

Sat_solver 
Interface to MSat

Sat_solver_intf  add_clause ~tag ~proof c adds the constraint c to the SAT solver,
annotated with proof .

Trail 
Boolean Trail

Ind_cst 
Inductive Constants and Cases

Cover_set 
Cover Set

Cut_form 
Universally Quantified Conjunction of Clauses

Phases 
Phases of the Prover

Phases_impl 
Implementation of Phases

Avatar 
Basic Splitting à la Avatar

Avatar_intf 
Split a clause into components

Induction 
Induction through Cut

Induction_intf 
Induction

Superposition 
Inference and simplification rules for the superposition calculus

Superposition_intf 
Term Indices

Rewriting 
Rewriting

EnumTypes 
Inference and simplification rules for "Enum Types"

Arith_int 
Cancellative Inferences on Integer Arithmetic

Arith_rat 
Cancellative Inferences on Rational Arithmetic

Heuristics 
Heuristics

Ind_types 
Deal with Inductive Types

Fool 
boolean subterms
