diff --git a/Dedukti.hs b/Dedukti.hs
--- a/Dedukti.hs
+++ b/Dedukti.hs
@@ -2,24 +2,23 @@
 -- Copyright : © 2009 CNRS - École Polytechnique - INRIA
 -- License   : GPL
 --
--- This module is the entry point for europa. Based on the command line
+-- This module is the entry point for Dedukti. Based on the command line
 -- arguments the appropriate driver is invoked. Everything is coordinated by
 -- the driver. This module is also the place where global configuration data
 -- is initialized.
 
 module Main where
 
-import System.Environment
 import qualified Dedukti.Config as Config
 import Dedukti.DkM
 import Dedukti.Module
 import Dedukti.Driver.Batch
 import Dedukti.Driver.Compile
+import System.Console.Option
 import Text.PrettyPrint.Leijen
-import Data.List (partition, isPrefixOf)
-import Data.Either (partitionEithers)
+import System.Environment
 import System.Exit
-import System.IO
+import System.IO (stderr)
 import qualified Data.ByteString.Lazy.Char8 as B
 import qualified Paths_dedukti as Cabal (version)
 import Data.Version
@@ -32,9 +31,6 @@
           | FlagVerbose | FlagVeryVerbose
             deriving (Eq, Ord, Show)
 
-data FlagArity a = Nullary String Flag
-                 | Unary String (String -> Flag)
-
 flagDescriptions =
   [ ([Nullary "--make" FlagMake],
      "Build MODULE and all its dependencies in one go.")
@@ -51,50 +47,11 @@
   , ([Nullary "--version" FlagVersion],
      "Output version information then exit.") ]
 
--- Flag descriptions obey the following conventions:
---
--- - double hyphen flags don't have arguments.
---
--- - Everything after the first letter of a hyphen flag is part of the
---   argument.
-parseCmdline args =
-  let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args
-      (errors, flags) = partitionEithers $ map toFlag hyphened
-  in (flags, rest, errors)
-    where flagmap = concatMap fst flagDescriptions
-          unpack ('-':'-':name) = (name, "")
-          unpack ('-':name:arg) = ([name], arg)
-          unpack x = error $ "Malformed argument: " ++ x
-          lookupFlag name arg (Nullary n f : desc)
-              | fst (unpack n) == name =
-                  if null arg
-                  then Right f
-                  else Left $ "No argument expected for flag " ++ n
-          lookupFlag name arg (Unary n f : desc)
-              | fst (unpack n) == name = Right (f arg)
-          lookupFlag name _ [] = Left $ "Flag not found: " ++ name
-          lookupFlag name arg (_:desc) = lookupFlag name arg desc
-          toFlag x | (name, arg) <- unpack x = lookupFlag name arg flagmap
-
-printUsage = do
-  self <- parameter Config.imageName
-  let header = show $ text "Usage:" <+>
-               (text self <+> text "[OPTION]..." <+> text "MODULE")
-  io $ hPutStrLn stderr header
-
-printHelp = do
-  self <- parameter Config.imageName
-  let header = text "Usage:" <+>
-               (text self <+> text "[OPTION]..." <+> text "MODULE")
-               <$> text "Options:"
-      flags = vsep (map pflag flagDescriptions)
-  io $ putStrLn $ show $ header <$> indent 4 flags
-    where pflag (flags, desc) = fillBreak 14 (hcat $ punctuate (text ", ") $
-                                   map (text . name) flags) <+> text desc
-          name (Nullary n _) = n
-          name (Unary n _) = n
+usage = do self <- parameter Config.imageName
+           return $ text "Usage:" <+>
+             (text self <+> text "[OPTION]..." <+> text "MODULE")
 
-bailout = printUsage >> io exitFailure
+bailout = usage >>= io . printUsage >> io exitFailure
 
 printVersion = do
   self <- parameter Config.imageName
@@ -114,13 +71,15 @@
 
 main = do
   args <- getArgs
-  let (opts, files, errs) = parseCmdline args
+  let (opts, files, errs) = parseCmdline flagDescriptions args
   when (not (null errs)) $ do
          hPutDoc stderr (vcat (map text errs) <> line)
          exitFailure
   (`runDkM` initializeConfiguration opts) $
          case undefined of
-           _ | FlagHelp `elem` opts -> printHelp
+           _ | FlagHelp `elem` opts -> do
+                     u <- usage
+                     io $ printHelp u flagDescriptions
              | FlagVersion `elem` opts -> printVersion
            _ | FlagMake `elem` opts -> do
                      unless (length files == 1) bailout
diff --git a/Dedukti/Analysis/Rule.hs b/Dedukti/Analysis/Rule.hs
--- a/Dedukti/Analysis/Rule.hs
+++ b/Dedukti/Analysis/Rule.hs
@@ -24,6 +24,8 @@
 
 instance Exception NonContiguousRules
 
+-- | All rules for a same constant must be given contiguously, without
+-- intervening rules for other constants.
 checkOrdering :: [TyRule Qid a] -> DkM ()
 checkOrdering rules = do
   say Verbose $ text "Checking rule contiguity ..."
diff --git a/Dedukti/CodeGen.hs b/Dedukti/CodeGen.hs
--- a/Dedukti/CodeGen.hs
+++ b/Dedukti/CodeGen.hs
@@ -17,6 +17,8 @@
     -- | Emit code corresponding to an individual rule set.
     emit :: RuleSet (Id o) (A o) -> o
 
+    -- | Combine code from a number of rule sets, typically forming a module,
+    -- into a bundle.
     coalesce :: [o] -> Bundle o
 
     -- | Produce the byte sequence to write to a file, given the code
diff --git a/Dedukti/Core.hs b/Dedukti/Core.hs
--- a/Dedukti/Core.hs
+++ b/Dedukti/Core.hs
@@ -76,6 +76,7 @@
 
 type Module id a = ([Binding id a], [TyRule id a])
 
+-- | Type families used to project out the type parameters from the datatypes.
 type family Id t
 type family A t
 
diff --git a/Dedukti/Driver/Batch.hs b/Dedukti/Driver/Batch.hs
--- a/Dedukti/Driver/Batch.hs
+++ b/Dedukti/Driver/Batch.hs
@@ -2,8 +2,9 @@
 -- Copyright : © 2009 CNRS - École Polytechnique - INRIA
 -- License   : GPL
 --
--- The batch driver. It compiles all given targets and all their dependencies,
--- also invoking the Haskell compiler on the generated source code.
+-- The batch driver. It compiles all given targets and all their dependencies
+-- (using the Compile driver), also invoking the Haskell compiler on the
+-- generated source code.
 
 module Dedukti.Driver.Batch (make) where
 
@@ -23,6 +24,7 @@
 import Data.Char (toUpper)
 
 
+-- The staleness check.
 cmp x y = do
   s <- io $ IO.isStale x y
   say Debug $ text "Compared" <+> text x <+> text y <> text ":" <+> text (show s)
diff --git a/Dedukti/Driver/Interactive.hs b/Dedukti/Driver/Interactive.hs
--- a/Dedukti/Driver/Interactive.hs
+++ b/Dedukti/Driver/Interactive.hs
@@ -11,6 +11,9 @@
 import Data.ByteString.Lazy (ByteString)
 
 
+dk = QuasiQuote { quoteExp = parse "<interactive>"
+                , quoteDec = undefined }
+
 -- | Emit Haskell code for one module.
 eval :: String -> ByteString
 eval input =
diff --git a/Dedukti/Module.hs b/Dedukti/Module.hs
--- a/Dedukti/Module.hs
+++ b/Dedukti/Module.hs
@@ -34,6 +34,7 @@
 import StringTable.Atom (Atom)
 
 
+-- | A generic stack-like datatype for representing hierarchical names.
 data Hierarchy = !Hierarchy :. !Atom | Root
                  deriving (Eq, Ord, Show)
 
diff --git a/System/Console/Option.hs b/System/Console/Option.hs
new file mode 100644
--- /dev/null
+++ b/System/Console/Option.hs
@@ -0,0 +1,57 @@
+-- |
+-- Copyright : © 2009 CNRS - École Polytechnique - INRIA
+-- License   : GPL
+--
+-- Parse command-line options (or flags).
+--
+-- Flag descriptions obey the following conventions:
+--
+-- * double hyphen flags don't have arguments.
+--
+-- * Everything after the first letter of a hyphen flag is part of the
+-- argument.
+
+module System.Console.Option where
+
+import Text.PrettyPrint.Leijen
+import Data.Either (partitionEithers)
+import Data.List (partition, isPrefixOf)
+import System.IO
+
+
+data FlagArity f = Nullary String f
+                 | Unary String (String -> f)
+
+type Description f = [([FlagArity f], String)]
+
+parseCmdline :: Description f -> [String] -> ([f], [String], [String])
+parseCmdline desc args =
+  let (hyphened, rest) = partition (\arg -> "-" `isPrefixOf` arg) args
+      (errors, flags) = partitionEithers $ map toFlag hyphened
+  in (flags, rest, errors)
+    where flagmap = concatMap fst desc
+          unpack ('-':'-':name) = (name, "")
+          unpack ('-':name:arg) = ([name], arg)
+          unpack x = error $ "Malformed argument: " ++ x
+          lookupFlag name arg (Nullary n f : desc)
+              | fst (unpack n) == name =
+                  if null arg
+                  then Right f
+                  else Left $ "No argument expected for flag " ++ n
+          lookupFlag name arg (Unary n f : desc)
+              | fst (unpack n) == name = Right (f arg)
+          lookupFlag name _ [] = Left $ "Flag not found: " ++ name
+          lookupFlag name arg (_:desc) = lookupFlag name arg desc
+          toFlag x | (name, arg) <- unpack x = lookupFlag name arg flagmap
+
+printUsage :: Doc -> IO ()
+printUsage = hPutStrLn stderr . show
+
+printHelp :: Doc -> Description f -> IO ()
+printHelp usage desc = do
+  let flags = vsep (map pflag desc)
+  putStrLn $ show $ usage <$> text "Options:" <$> indent 4 flags
+    where pflag (flags, desc) = fillBreak 14 (hcat $ punctuate (text ", ") $
+                                   map (text . name) flags) <+> text desc
+          name (Nullary n _) = n
+          name (Unary n _) = n
diff --git a/dedukti.cabal b/dedukti.cabal
--- a/dedukti.cabal
+++ b/dedukti.cabal
@@ -1,5 +1,5 @@
 name:           dedukti
-version:        1.1.2
+version:        1.1.3
 author:         Mathieu Boespflug
 maintainer:     Mathieu Boespflug <mboes@lix.polytechnique.fr>
 copyright:      © 2009 CNRS - École Polytechnique - INRIA
@@ -46,31 +46,31 @@
 
 library
   exposed-modules:     Dedukti.Runtime
-  build-depends:       time >= 1.1, unix >= 2.4
+  build-depends:       time >= 1.1, unix >= 2.3
   extensions:          DeriveDataTypeable, PatternGuards, FlexibleInstances
   ghc-options:         -fwarn-unused-binds -fwarn-unused-imports
 
 executable dedukti
   main-is:             Dedukti.hs
-  other-modules:       Dedukti.Core,
-                       Dedukti.Parser,
-                       Dedukti.Parser.External,
-                       Dedukti.Parser.Prefix,
-                       Dedukti.Parser.Interface,
-                       Dedukti.Pretty,
-                       Dedukti.Driver.Interactive,
-                       Dedukti.Driver.Batch,
-                       Dedukti.Driver.Compile,
-                       Dedukti.Rule,
-                       Dedukti.DkM,
-                       Dedukti.Config,
-                       Dedukti.Module,
+  other-modules:       Dedukti.Core
+                       Dedukti.Parser
+                       Dedukti.Parser.External
+                       Dedukti.Parser.Prefix
+                       Dedukti.Parser.Interface
+                       Dedukti.Pretty
+                       Dedukti.Driver.Interactive
+                       Dedukti.Driver.Batch
+                       Dedukti.Driver.Compile
+                       Dedukti.Rule
+                       Dedukti.DkM
+                       Dedukti.Config
+                       Dedukti.Module
                        Dedukti.CodeGen
-                       Dedukti.CodeGen.Exts,
-                       Dedukti.Analysis.Rule,
-                       Dedukti.Analysis.Scope,
+                       Dedukti.CodeGen.Exts
+                       Dedukti.Analysis.Rule
+                       Dedukti.Analysis.Scope
                        Dedukti.Analysis.Dependency
-
+                       System.Console.Option
   build-depends:       base >= 4 && < 5, mtl >= 1.1, containers >= 0.2,
                        directory, filepath, process,
                        bytestring >= 0.9.1.0,