diff --git a/Civilisation.hs b/Civilisation.hs
index bae7583..a3151b2 100644
--- a/Civilisation.hs
+++ b/Civilisation.hs
@@ -10,7 +10,14 @@ Portability :  portable
 
 -}
 
-module Civilisation where
+module Civilisation (
+  -- * DIMACS CNF parsing
+  parseDIMACS,
+  parseClause,
+  litFromInt,
+  -- * Main
+  main
+  ) where
 
 import Data.Maybe
 
diff --git a/Sat.hs b/Sat.hs
index 988e35f..d4cc9d2 100644
--- a/Sat.hs
+++ b/Sat.hs
@@ -11,7 +11,47 @@ Portability :  portable
 A simple SAT solver.
 -}
 
-module Sat where
+module Sat (
+  -- * Types
+  -- ** Literals, clauses and formulas
+  Var,
+  Lit(..),
+  Clause,
+  CNF,
+  -- ** Assignments and results
+  Assignment,
+  Result(..),
+  -- * General-purpose functions
+  fromLit,
+  isPos,
+  isNeg,
+  isClauseTrue,
+  notLit,
+  evalLit,
+  -- * Simple rules
+  -- ** Pure literal rule
+  testPureLit,
+  testPureVar,
+  eliminatePure,
+  posLits,
+  negLits,
+  pureLits,
+  pureLitRule,
+  -- ** Unit clause rule
+  eliminateUnits,
+  unitPropagate,
+  -- * Solvers
+  -- ** Resolution-rule solver
+  commonVar,
+  resolve,
+  findMatchingClause,
+  findMatchingPair,
+  resolveAll,
+  resolutionSolve,
+  -- ** DPLL solver
+  solveDPLL,
+  selectLit
+  ) where
 
 import Data.List