diff --git a/EqualitySolver.cabal b/EqualitySolver.cabal
--- a/EqualitySolver.cabal
+++ b/EqualitySolver.cabal
@@ -2,7 +2,7 @@
 -- documentation, see http://haskell.org/cabal/users-guide/
 
 name:                EqualitySolver
-version:             0.1.0.0
+version:             0.1.0.1
 synopsis:            A theory solver for conjunctions of literals in the theory of uninterpreted functions with equality
 -- description:         
 license:             BSD3
diff --git a/src/EqualitySolver/Solver.hs b/src/EqualitySolver/Solver.hs
--- a/src/EqualitySolver/Solver.hs
+++ b/src/EqualitySolver/Solver.hs
@@ -11,6 +11,9 @@
 import Data.Maybe
 import Data.Set as S
 
+-- |Returns true if the conjunction of literals given as an
+-- argument is satisfiable in the first order theory of
+-- uninterpreted functions with equality
 satisfiableInEq :: EqFormula -> Bool
 satisfiableInEq formula = fst $ runDecideEq $ decideEq formula
 
@@ -18,6 +21,7 @@
 data EqFormula = EqFormula (Set EqLiteral)
                  deriving (Eq, Ord, Show)
 
+-- |Build a conjunction of literals out of a list of literals
 eqF = EqFormula . S.fromList
 
 allTerms :: EqFormula -> [EqTerm]
@@ -36,7 +40,10 @@
   = EqLiteral Predicate EqTerm EqTerm
     deriving (Eq, Ord, Show)
 
+-- |'eq a b' builds the literal a = b
 eq = EqLiteral Eq
+
+-- |'neq a b' builds the literal 'not (a = b)'
 neq = EqLiteral Neq
 
 isEq (EqLiteral Eq _ _) = True
@@ -62,7 +69,9 @@
 showEqTerm (Function name arity args) = name ++ "(" ++ intercalate "," (L.map show args) ++ ")"
 showEqTerm (Variable name) = name
 
+-- |Returns a new variable
 var = Variable
+-- |Returns a new function
 fun = Function
 
 subTerms :: EqTerm -> [EqTerm]