diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -1,5 +1,9 @@
 # language-ats
 
-## Installation
+This is a package similar to
+[language-c](http://hackage.haskell.org/package/language-c) or
+[haskell-src-exts](http://hackage.haskell.org/package/haskell-src-exts) that
+provides a parser and pretty-printer for [ATS](http://ats-lang.org/).
 
-## Configuration
+The parser is buggy but it can handle a good subset of the language; check out
+the `test/data` directory for some examples of what is supported.
diff --git a/language-ats.cabal b/language-ats.cabal
--- a/language-ats.cabal
+++ b/language-ats.cabal
@@ -1,5 +1,5 @@
 name:                language-ats
-version:             0.1.1.11
+version:             0.1.1.12
 synopsis:            Parser and pretty-printer for ATS.
 description:         Parser and pretty-printer for [ATS](http://www.ats-lang.org/), written with Happy and Alex.
 license:             BSD3
@@ -10,7 +10,6 @@
 category:            Language, Lexer, Parser, Pretty Printer, ATS
 build-type:          Simple
 extra-doc-files:     README.md
-extra-source-files:  stack.yaml
 data-files:          test/data/*.dats
                    , test/data/*.sats
                    , test/data/*.out
diff --git a/src/Language/ATS/PrettyPrint.hs b/src/Language/ATS/PrettyPrint.hs
--- a/src/Language/ATS/PrettyPrint.hs
+++ b/src/Language/ATS/PrettyPrint.hs
@@ -193,8 +193,8 @@
         a (AddrAtF _ e)                = "addr@" <> e
         a (ViewAtF _ e)                = "view@" <> e
         a (ListLiteralF _ s t es)      = "list" <> string s <> "{" <> pretty t <> "}" <> prettyArgs es
-        a BinListF{} = undefined
         a CallF{} = undefined
+        a BinListF{} = undefined -- Shouldn't happen
         prettyImplicits = mconcat . fmap (prettyArgsU "<" ">") . reverse
         prettyIfCase []              = mempty
         prettyIfCase [(s, l, t)]     = "|" <+> s <+> pretty l <+> t
@@ -314,7 +314,7 @@
         where go (Arg (First s))  = pretty s
               go (Arg (Both s t)) = pretty s <+> colon <+> pretty t
               go (Arg (Second t)) = pretty t
-              go _                = undefined
+              go _                = undefined -- Shouldn't happen
 
 instance Pretty Universal where
     pretty (Universal [x@PrfArg{}] Nothing Nothing) = lbrace <+> pretty x <+> rbrace -- FIXME universals can now be length-one arguments
@@ -334,11 +334,11 @@
 prettyOr is = mconcat (fmap (prettyArgsU "<" ">") is)
 
 instance Pretty Implementation where
-    pretty (Implement _ [] is [] n [] e)  = "implement" <+> pretty n <> prettyOr is <+> "() =" <$> indent 2 (pretty e)
-    pretty (Implement _ [] is [] n ias e) = "implement" <+> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ [] is us n ias e) = "implement" <+> pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ ps is [] n ias e) = "implement" <+> foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
-    pretty (Implement _ ps is us n ias e) = "implement" <+> foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ [] is [] n [] e)  = pretty n <> prettyOr is <+> "() =" <$> indent 2 (pretty e)
+    pretty (Implement _ [] is [] n ias e) = pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ [] is us n ias e) = pretty n <> prettyOr is <+> foldMap pretty us </> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ ps is [] n ias e) = foldMap pretty ps </> pretty n <> prettyOr is <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
+    pretty (Implement _ ps is us n ias e) = foldMap pretty ps </> pretty n <> prettyOr is </> foldMap pretty us <+> prettyArgs ias <+> "=" <$> indent 2 (pretty e)
 
 isVal :: Declaration -> Bool
 isVal Val{}   = True
@@ -503,7 +503,9 @@
     pretty (SumViewType s as ls)           = "datavtype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls
     pretty (SumType s [] ls)               = "datatype" <+> text s <+> "=" <$> prettyLeaf ls
     pretty (SumType s as ls)               = "datatype" <+> text s <> prettyArgs as <+> "=" <$> prettyLeaf ls
-    pretty (Impl [] i)                     = pretty i
+    pretty (Impl [] i)                     = "implement" <+> pretty i
+    pretty (Impl us i)                     = "implement" <+> mconcat (fmap pretty us) <+> pretty i
+    pretty (ProofImpl i)                   = "primplmnt" <+> pretty i
     pretty (PrVal p e)                     = "prval" <+> pretty p <+> "=" <+> pretty e
     pretty (Val a Nothing p e)             = "val" <> pretty a <+> pretty p <+> "=" <+> pretty e
     pretty (Val a (Just t) p e)            = "val" <> pretty a <+> pretty p <> ":" <+> pretty t <+> "=" <+> pretty e
@@ -546,4 +548,8 @@
     pretty (Local _ d d')                  = "local" <$> indent 2 (pretty d) <$> "in" <$> indent 2 (pretty d') <$> "end"
     pretty (FixityDecl f (Left s) ss)      = pretty f <+> "(" <> text s <> ")" <+> hsep (fmap text ss)
     pretty (FixityDecl f (Right i) ss)     = pretty f <+> pretty i <+> hsep (fmap text ss)
+    pretty (StaVal us i t)                 = "val" </> mconcat (fmap pretty us) <+> text i <+> ":" <+> pretty t
+    pretty (Stadef i n [])                 = "stadef" <+> text i <+> pretty n
+    pretty (Stadef i n as)                 = "stadef" <+> text i <+> pretty n <> prettyArgs as
     pretty _                               = undefined
+
diff --git a/stack.yaml b/stack.yaml
deleted file mode 100644
--- a/stack.yaml
+++ /dev/null
@@ -1,10 +0,0 @@
----
-resolver: lts-10.3
-packages:
-  - '.'
-extra-deps:
-  - composition-prelude-1.1.0.0
-flags:
-  language-ats:
-    development: false
-extra-package-dbs: []