diff --git a/gdp.cabal b/gdp.cabal
--- a/gdp.cabal
+++ b/gdp.cabal
@@ -1,5 +1,5 @@
 name:                gdp
-version:             0.0.0.1
+version:             0.0.0.2
 synopsis:            Reason about invariants and preconditions with ghosts of departed proofs.
 description:         Reason about invariants and preconditions with ghosts of departed proofs.
                      The GDP library implements building blocks for creating and working with
diff --git a/src/Data/Refined.hs b/src/Data/Refined.hs
--- a/src/Data/Refined.hs
+++ b/src/Data/Refined.hs
@@ -109,7 +109,7 @@
 infixr 1 ?
 
 -- | For library authors: assert that a property holds.
-assert :: Defining (p n) => a -> (a ?p)
+assert :: Defining (p ()) => a -> (a ?p)
 assert x = name x (\x -> unname (x ...axiom))
 
 -- | Existential introduction for names: given a named value of
diff --git a/src/Theory/Equality.hs b/src/Theory/Equality.hs
--- a/src/Theory/Equality.hs
+++ b/src/Theory/Equality.hs
@@ -101,7 +101,7 @@
   Theory of equality
 --------------------------------------------------}
 
--- | Test if the two name arguments are equal an, if so, produce a proof
+-- | Test if the two named arguments are equal and, if so, produce a proof
 --   of equality for the names.
 same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))
 same (The x) (The y) = if x == y then Just axiom else Nothing