diff --git a/Display.hs b/Display.hs
--- a/Display.hs
+++ b/Display.hs
@@ -18,10 +18,6 @@
 (<>) :: Monoid a => a -> a -> a
 (<>) = mappend
 
-instance Monoid Doc where
-    mempty = empty
-    mappend = (Text.PrettyPrint.HughesPJ.<>)
-
 class Pretty a where
     pretty :: a -> Doc
 
@@ -30,9 +26,6 @@
 
 instance (Pretty a,Pretty b) => Pretty (a,b) where
     pretty (a,b) = parens $ pretty a <> comma <+> pretty b 
-
-instance IsString Doc where
-    fromString = text
 
 instance Pretty Int where
   pretty = int
diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -285,7 +285,9 @@
 
 swapCube :: Permutation -> Int -> Cube NF -> Cube NF
 swapCube q0 d c = apply q . subAppl q (\p -> swapNF p d) $ c
-  where q = reducePerm q0 (dim c) -- FIXME: reduction should never be necessary
+  where q = reducePerm q0 (dim c) -- FIXME: reduction should never be
+                                  -- necessary; we have dimension
+                                  -- checks.
 
 swapBinder :: Permutation -> Int -> Cube NF -> Cube NF
 swapBinder = swapCube
diff --git a/uAgda.cabal b/uAgda.cabal
--- a/uAgda.cabal
+++ b/uAgda.cabal
@@ -1,5 +1,5 @@
 name:           uAgda
-version:        1.2.0.1
+version:        1.2.0.2
 category:       Dependent Types
 synopsis:       A simplistic dependently-typed language with parametricity.
 description:
@@ -46,9 +46,9 @@
   build-depends: array==0.3.*
   build-depends: cmdargs==0.6.*
   build-depends: containers==0.4.*
-  build-depends: pretty==1.0.*
+  build-depends: pretty==1.1.*
   build-depends: parsec==2.1.*
-  build-depends: BNFC-meta==0.3.*
+  build-depends: BNFC-meta==0.2.*
   build-depends: transformers == 0.2.*
   build-depends: mtl == 2.0.*
   build-depends: split == 0.1.*