ClauseQueue 
Priority Queue of clauses

Clause 
Clauses

SClause 
Simple Clause

Const 
Configuration and Globals

Extensions 
Dynamic extensions

Literal 
Equational literals

Literals 
Array of literals

Ctx 
Basic context for literals, clauses...

ProofStep 
Manipulate proofs

ProofPrint 
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

Compute_prec 
Compute Precedence

Params 
Parameters for the prover, etc.

Env 
Global environment for an instance of the prover

Monome 
Polynomes of order 1, over several variables.

ArithLit 
Arithmetic Literal

Signals 
Useful signals

Multisets 
Several Multisets

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

Phases 
Phases of the Prover

Phases_impl 
Implementation of Phases

Flex_state 
Extensible Map for State

Classify_cst 
Classification of Constants

Rewrite_rule 
Rewrite Rules

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

Rewriting 
Rewriting

EnumTypes 
Inference and simplification rules for "Enum Types"

ArithInt 
Cancellative Inferences on Integer Arithmetic

Heuristics 
Heuristics

Ind_types 
Deal with Inductive Types

MetaProverState 
Meta Prover for zipperposition

MetaProverState_intf 
Rewrite system
