diff --git a/CHANGELOG.md b/CHANGELOG.md
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,3 +1,9 @@
+# New in 1.1.1
+
++ Erasure analysis is now faster thanks to a bit smarter constraint solving.
++ Fixed installation issue
++ Fixed a potential segfault when concatenating strings
+
 # New in 1.1.0
 
 ## Library Updates
diff --git a/Setup.hs b/Setup.hs
--- a/Setup.hs
+++ b/Setup.hs
@@ -1,11 +1,15 @@
 {-# LANGUAGE CPP #-}
 
+#if !defined(MIN_VERSION_Cabal)
+# define MIN_VERSION_Cabal(x,y,z) 0
+#endif
+
 import Control.Monad
 import Data.IORef
 import Control.Exception (SomeException, catch)
 
 import Distribution.Simple
-import Distribution.Simple.BuildPaths (autogenModulesDir)
+import Distribution.Simple.BuildPaths
 import Distribution.Simple.InstallDirs as I
 import Distribution.Simple.LocalBuildInfo as L
 import qualified Distribution.Simple.Setup as S
@@ -56,32 +60,37 @@
 
 usesGMP :: S.ConfigFlags -> Bool
 usesGMP flags =
-  case lookup (FlagName "gmp") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "gmp") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
 execOnly :: S.ConfigFlags -> Bool
 execOnly flags =
-  case lookup (FlagName "execonly") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "execonly") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
 isRelease :: S.ConfigFlags -> Bool
 isRelease flags =
-    case lookup (FlagName "release") (S.configConfigurationsFlags flags) of
+    case lookup (mkFlagName "release") (S.configConfigurationsFlags flags) of
       Just True -> True
       Just False -> False
       Nothing -> False
 
 isFreestanding :: S.ConfigFlags -> Bool
 isFreestanding flags =
-  case lookup (FlagName "freestanding") (S.configConfigurationsFlags flags) of
+  case lookup (mkFlagName "freestanding") (S.configConfigurationsFlags flags) of
     Just True -> True
     Just False -> False
     Nothing -> False
 
+#if !(MIN_VERSION_Cabal(2,0,0))
+mkFlagName :: String -> FlagName
+mkFlagName = FlagName
+#endif
+
 -- -----------------------------------------------------------------------------
 -- Clean
 
@@ -151,20 +160,22 @@
     createDirectoryIfMissingVerbose verbosity True srcDir
     rewriteFile toolPath (commonContent ++ toolContent)
 
-idrisConfigure _ flags _ local = do
+idrisConfigure _ flags pkgdesc local = do
     configureRTS
-    generateVersionModule verbosity (autogenModulesDir local) (isRelease (configFlags local))
-    if isFreestanding $ configFlags local
-        then do
-                toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
-                generateToolchainModule verbosity (autogenModulesDir local) toolDir
-                targetDir <- lookupEnv "IDRIS_LIB_DIR"
-                case targetDir of
-                     Just d -> generateTargetModule verbosity (autogenModulesDir local) d
-                     Nothing -> error $ "Trying to build freestanding without a target directory."
-                                  ++ " Set it by defining IDRIS_LIB_DIR."
-        else
-                generateToolchainModule verbosity (autogenModulesDir local) Nothing
+    withLibLBI pkgdesc local $ \_ libcfg -> do
+      let libAutogenDir = autogenComponentModulesDir local libcfg
+      generateVersionModule verbosity libAutogenDir (isRelease (configFlags local))
+      if isFreestanding $ configFlags local
+          then do
+                  toolDir <- lookupEnv "IDRIS_TOOLCHAIN_DIR"
+                  generateToolchainModule verbosity libAutogenDir toolDir
+                  targetDir <- lookupEnv "IDRIS_LIB_DIR"
+                  case targetDir of
+                       Just d -> generateTargetModule verbosity libAutogenDir d
+                       Nothing -> error $ "Trying to build freestanding without a target directory."
+                                    ++ " Set it by defining IDRIS_LIB_DIR."
+          else
+                  generateToolchainModule verbosity libAutogenDir Nothing
     where
       verbosity = S.fromFlag $ S.configVerbosity flags
       version   = pkgVersion . package $ localPkgDescr local
@@ -175,6 +186,10 @@
       -- the file after configure.
       configureRTS = make verbosity ["-C", "rts", "clean"]
 
+#if !(MIN_VERSION_Cabal(2,0,0))
+      autogenComponentModulesDir lbi _ = autogenModulesDir lbi
+#endif
+
 idrisPreSDist args flags = do
   let dir = S.fromFlag (S.sDistDirectory flags)
   let verb = S.fromFlag (S.sDistVerbosity flags)
@@ -225,9 +240,10 @@
         return (Nothing, [])
 #endif
 
-idrisBuild _ flags _ local = unless (execOnly (configFlags local)) $ do
-      buildStdLib
-      buildRTS
+idrisBuild _ flags _ local 
+   = if (execOnly (configFlags local)) then buildRTS
+        else do buildStdLib
+                buildRTS
    where
       verbosity = S.fromFlag $ S.buildVerbosity flags
 
@@ -246,10 +262,11 @@
 -- -----------------------------------------------------------------------------
 -- Copy/Install
 
-idrisInstall verbosity copy pkg local = unless (execOnly (configFlags local)) $ do
-      installStdLib
-      installRTS
-      installManPage
+idrisInstall verbosity copy pkg local 
+   = if (execOnly (configFlags local)) then installRTS
+        else do installStdLib
+                installRTS
+                installManPage
    where
       target = datadir $ L.absoluteInstallDirs pkg local copy
 
diff --git a/docs/reference/partial-evaluation.rst b/docs/reference/partial-evaluation.rst
--- a/docs/reference/partial-evaluation.rst
+++ b/docs/reference/partial-evaluation.rst
@@ -4,15 +4,15 @@
 
 As of version 0.9.15, Idris has support for *partial evaluation* of
 statically known arguments. This involves creating specialised versions
-of functions with arguments annotated as ``[static]``.
+of functions with arguments annotated as ``%static``.
 
 (This is an implementation of the partial evaluator described in `this
 ICFP 2010
 paper <http://eb.host.cs.st-andrews.ac.uk/writings/icfp10.pdf>`__.
 Please refer to this for more precise definitions of what follows.)
 
-Partial evaluation is switched on by default. It can be disabled with
-the ``--no-partial-eval`` flag.
+Partial evaluation is switched off by default since Idris 1.0. It can
+be enabled with the ``--partial-eval`` flag.
 
 Introductory Example
 --------------------
@@ -66,18 +66,18 @@
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 
 The trick is to mark the statically known arguments with the
-``[static]`` flag:
+``%static`` flag:
 
 ::
 
-    my_pow : Nat -> [static] Nat -> Nat
+    my_pow : Nat -> %static Nat -> Nat
     my_pow k Z = 1
     my_pow k (S j) = mult k (my_pow k j)
 
 When an argument is annotated in this way, Idris will try to create a
 specialised version whenever it accounts a call with a concrete value
 (i.e. a constant, constructor form, or globally defined function) in a
-``[static]`` position. If ``my_pow`` is defined this way, and ``powFn``
+``%static`` position. If ``my_pow`` is defined this way, and ``powFn``
 defined as above, we can see the effect by typing ``:printdef powFn`` at
 the REPL:
 
@@ -108,7 +108,7 @@
 -------------------------
 
 Type class dictionaries are very often statically known, so Idris
-automatically marks any type class constraint as ``[static]`` and builds
+automatically marks any type class constraint as ``%static`` and builds
 specialised versions of top level functions where the class is
 instantiated. For example, given:
 
@@ -177,7 +177,7 @@
 
 ::
 
-    my_map : [static] (a -> b) -> List a -> List b
+    my_map : %static (a -> b) -> List a -> List b
     my_map f [] = []
     my_map f (x :: xs) = f x :: my_map f xs
 
@@ -246,11 +246,11 @@
                 (App (App eMult (App eFac (Op (-) x (Val 1)))) x))
 
 The interpreter's type is written as follows, marking the expression to
-be evaluated as ``[static]``:
+be evaluated as ``%static``:
 
 ::
 
-    interp : (env : Env gamma) -> [static] (e : Expr gamma t) -> interpTy t
+    interp : (env : Env gamma) -> %static (e : Expr gamma t) -> interpTy t
 
 This means that if we write an Idris program to calculate a factorial by
 calling ``interp`` on ``eFac``, the resulting definition will be
diff --git a/idris.cabal b/idris.cabal
--- a/idris.cabal
+++ b/idris.cabal
@@ -1,5 +1,5 @@
 Name:           idris
-Version:        1.1.0
+Version:        1.1.1
 License:        BSD3
 License-file:   LICENSE
 Author:         Edwin Brady
@@ -44,7 +44,7 @@
 
 Build-type:     Custom
 
-Tested-With:    GHC == 7.6.3, GHC == 7.8.4, GHC == 7.10.3, GHC == 8.0.1
+Tested-With:    GHC == 7.10.3, GHC == 8.0.1
 
 Data-files:            idrisdoc/styles.css
                        jsrts/jsbn/jsbn-browser.js
@@ -97,6 +97,14 @@
   type:     git
   location: git://github.com/idris-lang/Idris-dev.git
 
+custom-setup
+  setup-depends:
+    Cabal >= 1.10 && <2.1,
+    base  >= 4 && <5,
+    directory,
+    filepath,
+    process
+
 Flag FFI
   Description:  Build support for libffi
   Default:      False
@@ -111,7 +119,7 @@
 -- Defaults to True because Hackage is a source release
 Flag release
   Description:  This is an official release
-  Default:      True
+  Default:      False
   manual:       True
 
 Flag freestanding
@@ -259,17 +267,17 @@
                 , Tools_idris
 
   Build-depends:  base >=4 && <5
-                , aeson >= 0.6 && < 1.2
+                , aeson >= 0.6 && < 1.3
                 , annotated-wl-pprint >= 0.7 && < 0.8
                 , ansi-terminal < 0.7
                 , ansi-wl-pprint < 0.7
                 , array >= 0.4.0.1 && < 0.6
                 , base64-bytestring < 1.1
-                , binary >= 0.7 && < 0.9
+                , binary >= 0.8.4.1 && < 0.9
                 , blaze-html >= 0.6.1.3 && < 0.10
                 , blaze-markup >= 0.5.2.1 && < 0.9
                 , bytestring < 0.11
-                , cheapskate < 0.2
+                , cheapskate >= 0.1.1 && < 0.2
                 , code-page >= 0.1 && < 0.2
                 , containers >= 0.5 && < 0.6
                 , deepseq < 1.5
@@ -277,20 +285,22 @@
                 , filepath < 1.5
                 , fingertree >= 0.1 && < 0.2
                 , haskeline >= 0.7 && < 0.8
-                , ieee754 >= 0.7 && <= 0.8.0
+                , ieee754 >= 0.7 && < 0.9
                 , mtl >= 2.1 && < 2.3
                 , network < 2.7
-                , optparse-applicative >= 0.13 && < 0.14
+                , optparse-applicative >= 0.13 && < 0.15
                 , parsers >= 0.9 && < 0.13
                 , pretty < 1.2
+                , process < 1.7
                 , regex-tdfa >= 1.2
+                , safe >= 0.3.9
                 , split < 0.3
                 , terminal-size < 0.4
                 , text >=1.2.1.0 && < 1.3
-                , time >= 1.4 && < 1.7
+                , time >= 1.4 && < 1.9
                 , transformers < 0.6
                 , transformers-compat >= 0.3
-                , trifecta >= 1.6 && < 1.7
+                , trifecta >= 1.6 && < 1.8
                 , uniplate >=1.6 && < 1.7
                 , unordered-containers < 0.3
                 , utf8-string < 1.1
@@ -300,41 +310,14 @@
                 , fsnotify >= 0.2 && < 2.2
                 , async < 2.2
 
-
-  -- zlib >= 0.6.1 is broken with GHC < 7.10.3
-  -- Travis is broken for 7.6 and 7.8 with a newer process
-  if impl(ghc < 7.10.3)
-     build-depends: zlib < 0.6.1
-                  , process < 1.3
-  else
-     build-depends: process < 1.5
-
-  -- safe 0.3.10 is having issues with cabal 1.20 and ghc 7.6.3, the
-  -- hvr ghc ppa doesn't provide a new enough cabal library. Temporary
-  -- fix until hvr ghc ppa is fixed or we deprecate support for 7.6.3.
-  if impl(ghc < 7.8.4)
-     build-depends: safe == 0.3.9
-  else
-     build-depends: safe >= 0.3.9
-
-  if impl(ghc < 7.8.4)
-     build-depends: tagsoup < 0.14.1
-
   Default-Language: Haskell2010
-
   ghc-prof-options: -auto-all -caf-all
 
-  if os(linux)
-     build-depends: unix < 2.8
-  if os(freebsd)
-     build-depends: unix < 2.8
---   if os(dragonfly)
---      build-depends: unix < 2.8
-  if os(darwin)
-     build-depends: unix < 2.8
   if os(windows)
      build-depends: mintty >= 0.1 && < 0.2
                   , Win32 < 2.4
+  else
+     build-depends: unix < 2.8
   if flag(FFI)
      build-depends: libffi < 0.2
      cpp-options:   -DIDRIS_FFI
diff --git a/jsrts/Runtime-node.js b/jsrts/Runtime-node.js
--- a/jsrts/Runtime-node.js
+++ b/jsrts/Runtime-node.js
@@ -22,7 +22,7 @@
         }
         i++;
         if (i == b.length) {
-            nb = new Buffer(b.length * 2);
+            var nb = new Buffer(b.length * 2);
             b.copy(nb)
             b = nb;
         }
diff --git a/libs/contrib/Text/Lexer.idr b/libs/contrib/Text/Lexer.idr
--- a/libs/contrib/Text/Lexer.idr
+++ b/libs/contrib/Text/Lexer.idr
@@ -23,11 +23,11 @@
 inf : Bool -> Type -> Type
 inf True t = Inf t
 inf False t = t
-  
+
 ||| Sequence two recognisers. If either consumes a character, the sequence
 ||| is guaranteed to consume a character.
 export %inline
-(<+>) : {c1 : Bool} -> 
+(<+>) : {c1 : Bool} ->
         Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)
 (<+>) {c1 = False} = SeqEmpty
 (<+>) {c1 = True} = SeqEat
@@ -59,6 +59,17 @@
 many : Lexer -> Recognise False
 many l = some l <|> Empty
 
+||| Recognise many instances of `l` until an instance of `end` is
+||| encountered.
+|||
+||| Useful for defining comments.
+export
+manyTill : (l : Lexer)
+        -> (end : Lexer) -> Recognise False
+manyTill l end = end
+             <|> (l <+> manyTill l end)
+             <|> Empty
+
 ||| Recognise any character
 export
 any : Lexer
@@ -86,7 +97,7 @@
 getString (MkStrLen str n) = str
 
 strIndex : StrLen -> Nat -> Maybe Char
-strIndex (MkStrLen str len) i 
+strIndex (MkStrLen str len) i
     = if i >= len then Nothing
                   else Just (assert_total (prim__strIndex str (cast i)))
 
@@ -102,25 +113,25 @@
 scan : Recognise c -> Nat -> StrLen -> Maybe Nat
 scan Empty idx str = pure idx
 scan Fail idx str = Nothing
-scan (Pred f) idx str 
+scan (Pred f) idx str
     = do c <- strIndex str idx
          if f c
             then Just (idx + 1)
             else Nothing
-scan (SeqEat r1 r2) idx str 
+scan (SeqEat r1 r2) idx str
     = do idx' <- scan r1 idx str
          -- TODO: Can we prove totality instead by showing idx has increased?
          assert_total (scan r2 idx' str)
-scan (SeqEmpty r1 r2) idx str 
+scan (SeqEmpty r1 r2) idx str
     = do idx' <- scan r1 idx str
          scan r2 idx' str
-scan (Alt r1 r2) idx str 
+scan (Alt r1 r2) idx str
     = case scan r1 idx str of
            Nothing => scan r2 idx str
            Just idx => Just idx
 
 takeToken : Lexer -> StrLen -> Maybe (String, StrLen)
-takeToken lex str 
+takeToken lex str
     = do i <- scan lex 0 str -- i must be > 0 if successful
          pure (substr 0 i (getString str), strTail i str)
 
@@ -134,7 +145,7 @@
 exact : String -> Lexer
 exact str with (unpack str)
   exact str | [] = Fail -- Not allowed, Lexer has to consume
-  exact str | (x :: xs) 
+  exact str | (x :: xs)
       = foldl SeqEmpty (is x) (map is xs)
 
 ||| Recognise a whitespace character
@@ -185,8 +196,8 @@
 
 fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)
 fspanEnd k p "" = (k, "")
-fspanEnd k p xxs 
-    = assert_total $ 
+fspanEnd k p xxs
+    = assert_total $
       let x = prim__strHead xxs
           xs = prim__strTail xxs in
           if p x then fspanEnd (S k) p xs
@@ -195,14 +206,14 @@
 -- Faster version of 'span' from the prelude (avoids unpacking)
 export
 fspan : (Char -> Bool) -> String -> (String, String)
-fspan p xs 
+fspan p xs
     = let (end, rest) = fspanEnd 0 p xs in
           (substr 0 end xs, rest)
 
 tokenise : (line : Int) -> (col : Int) ->
-           List (TokenData a) -> TokenMap a -> 
+           List (TokenData a) -> TokenMap a ->
            StrLen -> (List (TokenData a), (Int, Int, StrLen))
-tokenise line col acc tmap str 
+tokenise line col acc tmap str
     = case getFirstToken tmap str of
            Just (tok, line', col', rest) =>
            -- assert total because getFirstToken must consume something
@@ -213,7 +224,7 @@
     countNLs str = List.length (filter (== '\n') str)
 
     getCols : String -> Int -> Int
-    getCols x c 
+    getCols x c
          = case fspan (/= '\n') (reverse x) of
                 (incol, "") => c + cast (length incol)
                 (incol, _) => cast (length incol)
@@ -223,7 +234,7 @@
     getFirstToken ((lex, fn) :: ts) str
         = case takeToken lex str of
                Just (tok, rest) => Just (MkToken line col (fn tok),
-                                         line + cast (countNLs (unpack tok)), 
+                                         line + cast (countNLs (unpack tok)),
                                          getCols tok col, rest)
                Nothing => getFirstToken ts str
 
@@ -235,4 +246,3 @@
 lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))
 lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in
                    (ts, (l, c, getString str'))
-
diff --git a/libs/contrib/Text/Parser.idr b/libs/contrib/Text/Parser.idr
--- a/libs/contrib/Text/Parser.idr
+++ b/libs/contrib/Text/Parser.idr
@@ -3,7 +3,7 @@
 %default total
 
 -- TODO: Add some primitives for helping with error messages.
--- e.g. perhaps set a string to state what we're currently trying to 
+-- e.g. perhaps set a string to state what we're currently trying to
 -- parse, or to say what the next expected token is in words
 
 ||| Description of a language's grammar. The `tok` parameter is the type
@@ -26,14 +26,14 @@
                 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->
                 Grammar tok (c1 || c2) b
      Alt : {c1, c2 : Bool} ->
-           Grammar tok c1 ty -> Grammar tok c2 ty -> 
+           Grammar tok c1 ty -> Grammar tok c2 ty ->
            Grammar tok (c1 && c2) ty
 
 public export
 inf : Bool -> Type -> Type
 inf True t = Inf t
 inf False t = t
-  
+
 ||| Sequence two grammars. If either consumes some input, the sequence is
 ||| guaranteed to consume some input. If the first one consumes input, the
 ||| second is allowed to be recursive (because it means some input has been
@@ -44,11 +44,11 @@
         Grammar tok (c1 || c2) b
 (>>=) {c1 = False} = SeqEmpty
 (>>=) {c1 = True} = SeqEat
-    
+
 ||| Give two alternative grammars. If both consume, the combination is
 ||| guaranteed to consume.
 export
-(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty -> 
+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->
         Grammar tok (c1 && c2) ty
 (<|>) = Alt
 
@@ -82,21 +82,21 @@
 eof : Grammar tok False ()
 eof = EOF
 
-||| Commit to an alternative; if the current branch of an alternative 
+||| Commit to an alternative; if the current branch of an alternative
 ||| fails to parse, no more branches will be tried
 export
 commit : Grammar tok False ()
 commit = Commit
 
 data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where
-     Failure : {xs : List tok} -> 
+     Failure : {xs : List tok} ->
                (committed : Bool) ->
                (err : String) -> (rest : List tok) -> ParseResult xs c ty
      EmptyRes : (committed : Bool) ->
                 (val : ty) -> (more : List tok) -> ParseResult more False ty
      NonEmptyRes : (committed : Bool) ->
                    (val : ty) -> (more : List tok) ->
-                   ParseResult (x :: xs ++ more) c ty 
+                   ParseResult (x :: xs ++ more) c ty
 
 weakenRes : {whatever, c : Bool} -> {xs : List tok} ->
             ParseResult xs c ty -> ParseResult xs (whatever && c) ty
@@ -105,13 +105,13 @@
 weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs
 weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more
 
-shorter : (more : List tok) -> .(ys : List tok) -> 
+shorter : (more : List tok) -> .(ys : List tok) ->
           LTE (S (length more)) (S (length (ys ++ more)))
 shorter more [] = lteRefl
 shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))
 
 doParse : {c : Bool} ->
-          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) -> 
+          (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->
           ParseResult xs c ty
 doParse com xs act with (sizeAccessible xs)
   doParse com xs (Empty val) | sml = EmptyRes com val xs
@@ -120,17 +120,17 @@
   doParse com xs Commit | sml = EmptyRes True () xs
 
   doParse com [] (Terminal f) | sml = Failure com "End of input" []
-  doParse com (x :: xs) (Terminal f) | sml 
+  doParse com (x :: xs) (Terminal f) | sml
         = maybe
              (Failure com "Unrecognised token" (x :: xs))
              (\a => NonEmptyRes com {xs=[]} a xs)
              (f x)
   doParse com [] EOF | sml = EmptyRes com () []
-  doParse com (x :: xs) EOF | sml 
+  doParse com (x :: xs) EOF | sml
         = Failure com "Expected end of input" (x :: xs)
   doParse com [] (NextIs f) | sml = Failure com "End of input" []
-  doParse com (x :: xs) (NextIs f) | sml 
-        = if f x 
+  doParse com (x :: xs) (NextIs f) | sml
+        = if f x
              then EmptyRes com x (x :: xs)
              else Failure com "Unrecognised token" (x :: xs)
   doParse com xs (Alt x y) | sml with (doParse False xs x | sml)
@@ -140,19 +140,19 @@
                then Failure com msg ts
                else weakenRes (doParse False xs y | sml)
     -- Successfully parsed the first option, so use the outer commit flag
-    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs) 
+    doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)
           = EmptyRes com val xs
-    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more) 
+    doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)
           = NonEmptyRes com val more
   doParse com xs (SeqEmpty act next) | (Access morerec)
           = case doParse com xs act | Access morerec of
                  Failure com msg ts => Failure com msg ts
-                 EmptyRes com val xs => 
+                 EmptyRes com val xs =>
                        case doParse com xs (next val) | (Access morerec) of
                             Failure com' msg ts => Failure com' msg ts
                             EmptyRes com' val xs => EmptyRes com' val xs
                             NonEmptyRes com' val more => NonEmptyRes com' val more
-                 NonEmptyRes {x} {xs=ys} com val more => 
+                 NonEmptyRes {x} {xs=ys} com val more =>
                        case (doParse com more (next val) | morerec _ (shorter more ys)) of
                             Failure com' msg ts => Failure com' msg ts
                             EmptyRes com' val _ => NonEmptyRes com' val more
@@ -160,13 +160,13 @@
                                  rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
                                          NonEmptyRes com' val more'
   doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)
-    doParse com xs (SeqEat act next) | sml | Failure com' msg ts 
+    doParse com xs (SeqEat act next) | sml | Failure com' msg ts
          = Failure com' msg ts
-    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more) 
+    doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)
          = case doParse com' more (next val) | morerec _ (shorter more ys) of
                 Failure com' msg ts => Failure com' msg ts
                 EmptyRes com' val _ => NonEmptyRes com' val more
-                NonEmptyRes {x=x1} {xs=xs1} com' val more' => 
+                NonEmptyRes {x=x1} {xs=xs1} com' val more' =>
                      rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in
                              NonEmptyRes com' val more'
   -- This next line is not strictly necessary, but it stops the coverage
@@ -180,7 +180,7 @@
 ||| returns a pair of the parse result and the unparsed tokens (the remaining
 ||| input).
 export
-parse : (xs : List tok) -> (act : Grammar tok c ty) -> 
+parse : (xs : List tok) -> (act : Grammar tok c ty) ->
         Either (ParseError tok) (ty, List tok)
 parse xs act
     = case doParse False xs act of
@@ -190,7 +190,7 @@
 
 ||| Parse one or more things
 export
-some : Grammar tok True a -> 
+some : Grammar tok True a ->
        Grammar tok True (List a)
 some p = do x <- p
             (do xs <- some p
@@ -198,14 +198,14 @@
 
 ||| Parse zero or more things (may match the empty input)
 export
-many : Grammar tok True a -> 
+many : Grammar tok True a ->
        Grammar tok False (List a)
 many p = some p
      <|> pure []
 
 ||| Parse one or more things, separated by another thing
 export
-sepBy1 : Grammar tok True () -> Grammar tok True a -> 
+sepBy1 : Grammar tok True () -> Grammar tok True a ->
          Grammar tok True (List a)
 sepBy1 sep p = do x <- p
                   (do sep
@@ -215,7 +215,7 @@
 ||| Parse zero or more things, separated by another thing. May
 ||| match the empty input.
 export
-sepBy : Grammar tok True () -> Grammar tok True a -> 
+sepBy : Grammar tok True () -> Grammar tok True a ->
         Grammar tok False (List a)
 sepBy sep p = sepBy1 sep p <|> pure []
 
@@ -227,3 +227,44 @@
 optional p def = p <|> pure def
 
 
+||| Parse an instance of `p` that is between `left` and `right`.
+export
+between : (left  : Grammar tok True ())
+       -> (right : Grammar tok True ())
+       -> (p     : Grammar tok True a)
+       -> Grammar tok True a
+between left right contents = do
+   left
+   res <- contents
+   right
+   pure res
+
+||| Parse one or more instances of `p` separated by `s`, returning the
+||| parsed items and proof the resulting list is non-empty.
+export
+sepBy1' : (sep : Grammar tok True ())
+       -> (p   : Grammar tok True a)
+       -> Grammar tok True (xs : List a ** NonEmpty xs)
+sepBy1' sep p
+    = do x <- p
+         (do sep
+             xs <- sepBy1 sep p
+             pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
+
+||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.
+export
+some' : (p : Grammar tok True a)
+     -> Grammar tok True (xs : List a ** NonEmpty xs)
+some' p = do
+   x <- p
+   (do xs <- some p
+       pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)
+
+
+||| Optionally parse a thing. If the grammar provides a default use `optional` instead.
+export
+maybe : Grammar tok True a
+     -> Grammar tok False (Maybe a)
+maybe p =
+      (do res <- p; pure $ Just res)
+  <|> pure Nothing
diff --git a/libs/contrib/Text/PrettyPrint/WL/Characters.idr b/libs/contrib/Text/PrettyPrint/WL/Characters.idr
--- a/libs/contrib/Text/PrettyPrint/WL/Characters.idr
+++ b/libs/contrib/Text/PrettyPrint/WL/Characters.idr
@@ -69,8 +69,8 @@
 tick : Doc
 tick = char '`'
 
-tilda : Doc
-tilda = char '~'
+tilde : Doc
+tilde = char '~'
 
 hash : Doc
 hash = char '#'
diff --git a/libs/contrib/Text/PrettyPrint/WL/Core.idr b/libs/contrib/Text/PrettyPrint/WL/Core.idr
--- a/libs/contrib/Text/PrettyPrint/WL/Core.idr
+++ b/libs/contrib/Text/PrettyPrint/WL/Core.idr
@@ -128,10 +128,10 @@
 showPrettyDoc doc = showPrettyDocS doc ""
   where
     showPrettyDocS : (doc : PrettyDoc) -> (acc : String) -> String
-    showPrettyDocS Empty               = id
-    showPrettyDocS (Chara c rest)      = strCons c . showPrettyDocS rest
-    showPrettyDocS (Text len str rest) = (str ++) . showPrettyDocS rest
-    showPrettyDocS (Line lvl rest)     = (('\n' `strCons` indentation lvl) ++) . showPrettyDocS rest
+    showPrettyDocS Empty               acc = acc
+    showPrettyDocS (Chara c rest)      acc = strCons c (showPrettyDocS rest acc)
+    showPrettyDocS (Text len str rest) acc = str ++ (showPrettyDocS rest acc)
+    showPrettyDocS (Line lvl rest)     acc = (strCons '\n' (indentation lvl)) ++ showPrettyDocS rest acc
 
 private
 fits : (w : Int) -> (x : PrettyDoc) -> Bool
diff --git a/libs/prelude/Prelude/Bits.idr b/libs/prelude/Prelude/Bits.idr
--- a/libs/prelude/Prelude/Bits.idr
+++ b/libs/prelude/Prelude/Bits.idr
@@ -21,12 +21,12 @@
 -- Convert to `List Bits8`
 --------------------------------------------------------------------------------
 
-||| Convert to list of `Bits8` with the most signficant byte at the
+||| Convert to list of `Bits8` with the most significant byte at the
 ||| head.
 b8ToBytes : Bits8 -> List Bits8
 b8ToBytes b = [b]
 
-||| Convert to list of `Bits8` with the most signficant byte at the
+||| Convert to list of `Bits8` with the most significant byte at the
 ||| head.
 b16ToBytes : Bits16 -> List Bits8
 b16ToBytes b =
@@ -34,7 +34,7 @@
   , prim__truncB16_B8 b
   ]
 
-||| Convert to list of `Bits8` with the most signficant byte at the
+||| Convert to list of `Bits8` with the most significant byte at the
 ||| head.
 b32ToBytes : Bits32 -> List Bits8
 b32ToBytes b =
@@ -44,7 +44,7 @@
   , prim__truncB32_B8 b
   ]
 
-||| Convert to list of `Bits8` with the most signficant byte at the
+||| Convert to list of `Bits8` with the most significant byte at the
 ||| head.
 b64ToBytes : Bits64 -> List Bits8
 b64ToBytes b =
diff --git a/libs/prelude/Prelude/List.idr b/libs/prelude/Prelude/List.idr
--- a/libs/prelude/Prelude/List.idr
+++ b/libs/prelude/Prelude/List.idr
@@ -378,7 +378,7 @@
 scanl f q []      = [q]
 scanl f q (x::xs) = q :: scanl f (f q x) xs
 
-||| The scanl1 function is a variant of scanl that doesn't require an explicit 
+||| The scanl1 function is a variant of scanl that doesn't require an explicit
 ||| starting value.
 ||| It assumes the first element of the list to be the starting value and then
 ||| starts the fold with the element following it.
@@ -854,6 +854,10 @@
 --------------------------------------------------------------------------------
 -- Properties
 --------------------------------------------------------------------------------
+
+||| (::) is injective
+consInjective : (x :: xs) = (y :: ys) -> (x = y, xs = ys)
+consInjective Refl = (Refl, Refl)
 
 ||| The empty list is a right identity for append.
 appendNilRightNeutral : (l : List a) ->
diff --git a/libs/pruviloj/Pruviloj/Core.idr b/libs/pruviloj/Pruviloj/Core.idr
--- a/libs/pruviloj/Pruviloj/Core.idr
+++ b/libs/pruviloj/Pruviloj/Core.idr
@@ -225,13 +225,16 @@
         countPi (RBind _ (Pi _ _) body) = S (countPi body)
         countPi _ = Z
 
+||| A helper to extract the type representation for term.
+getTTType : Raw -> Elab TT
+getTTType r = snd <$> check !getEnv r
 
 ||| Split a pair into its projections, binding them in the context
 ||| with the supplied names. A special case of Coq's `inversion`.
 both : Raw -> TTName -> TTName -> Elab ()
 both tm n1 n2 =
     do -- We don't know that the term is canonical, so let-bind projections applied to it
-       (A, B) <- isPairTy (snd !(check !getEnv tm))
+       (A, B) <- isPairTy !(getTTType tm)
        remember n1 A; apply `(fst {a=~A} {b=~B} ~tm) []; solve
        remember n2 B; apply `(snd {a=~A} {b=~B} ~tm) []; solve
   where
@@ -253,7 +256,6 @@
        try (unproduct (Var n1))
        try (unproduct (Var n2))
 
-
 ||| A special-purpose tactic that attempts to solve a goal using
 ||| `Refl`. This is useful for ensuring that goals in fact are trivial
 ||| when developing or testing other tactics; otherwise, consider
@@ -268,3 +270,47 @@
                 , NamePart `{reflexivity}
                 , TextPart "is not applicable."
                 ]
+
+||| Attempt to swap the sides of equality in a goal. If the goal is `x = y`,
+||| after the invocation the focus will be on a hole of type `y = x`.
+symmetry : Elab ()
+symmetry =
+    do [_,_,_,_,res] <- apply (Var `{{sym}}) [True, True, True, True, False]
+          | _ => fail [TextPart "Failed while applying", NamePart `{symmetry}]
+       solve
+       focus res
+
+||| Swap the sides of an equality, saving the result in a `let`-binding.
+||| Returns the generated name.
+|||
+||| @ t the equality proof to swap
+||| @ hint a hint to use for generating the variable name for the result
+symmetryAs : (t : Raw) -> (hint : String) -> Elab TTName
+symmetryAs t hint =
+    case !(getTTType t) of
+      `((=) {A=~A} {B=~B} ~l ~r) =>
+        do af <- forget A
+           bf <- forget B
+           lf <- forget l
+           rf <- forget r
+           let ts = the Raw $ `(sym {a=~af} {b=~bf} {left=~lf} {right=~rf} ~t)
+           n <- gensym hint
+           letbind n !(forget !(getTTType ts)) ts
+           pure n
+      tt => fail [TermPart tt, TextPart "is not an equality"]
+
+||| Apply a function term to an argument term, saving the result in a
+||| `let`-binding. Returns the generated name.
+|||
+||| @ f the function to apply
+||| @ x the term to apply to
+||| @ hint a hint to use for generating the variable name for the result
+applyAs : (f : Raw) -> (x : Raw) -> (hint : String) -> Elab TTName
+applyAs f x hint =
+    case !(getTTType f) of
+      `(~xty -> ~yty) =>
+         do let fx = RApp f x
+            n <- gensym hint
+            letbind n !(forget !(getTTType fx)) fx
+            pure n
+      ftt => fail [TermPart ftt, TextPart "is not a function"]
diff --git a/rts/idris_rts.c b/rts/idris_rts.c
--- a/rts/idris_rts.c
+++ b/rts/idris_rts.c
@@ -460,6 +460,11 @@
     case CT_STRING:
         printf("STR[%s]", v->info.str.str);
         break;
+    case CT_STROFFSET:
+        printf("OFFSET[");
+        dumpVal((VAL)(v->info.str_offset->str));
+        printf("]");
+        break;
     case CT_FWD:
         printf("CT_FWD ");
         dumpVal((VAL)(v->info.ptr));
@@ -591,15 +596,16 @@
 VAL idris_concat(VM* vm, VAL l, VAL r) {
     char *rs = GETSTR(r);
     char *ls = GETSTR(l);
-    // dumpVal(l);
-    // printf("\n");
-    Closure* cl = allocate(sizeof(Closure) + GETSTRLEN(l) + GETSTRLEN(r) + 1, 0);
+    int llen = GETSTRLEN(l);
+    int rlen = GETSTRLEN(r);
+
+    Closure* cl = allocate(sizeof(Closure) + llen + rlen + 1, 0);
     SETTY(cl, CT_STRING);
     cl->info.str.str = (char*)cl + sizeof(Closure);
     strcpy(cl->info.str.str, ls);
     strcat(cl->info.str.str, rs);
 
-    cl->info.str.len = GETSTRLEN(l) + GETSTRLEN(r);
+    cl->info.str.len = llen + rlen;
     return cl;
 }
 
diff --git a/scripts/runidris b/scripts/runidris
--- a/scripts/runidris
+++ b/scripts/runidris
@@ -9,10 +9,17 @@
     mkdir $RUNIDRIS_DIR
     chmod 700 $RUNIDRIS_DIR
 fi
-TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`"
+
+OS=`uname -s`
+case $OS in
+    OpenBSD ) TEMP_NAME="runidris-`sha1 -q $1`" ;;
+          * ) TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`" ;;
+esac
+
 FP="$RUNIDRIS_DIR/$TEMP_NAME"
+cp "$1" "$FP.idr" # idris won't compile the script unless it ends in .idr
 if [ ! -e $FP ]; then
-    "${IDRIS:-idris}" $1 --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
+    "${IDRIS:-idris}" "$FP.idr" --ibcsubdir "$RUNIDRIS_DIR" -i "." -o $FP
 fi
 shift
 "$FP" "$@"
diff --git a/scripts/runidris-node b/scripts/runidris-node
--- a/scripts/runidris-node
+++ b/scripts/runidris-node
@@ -9,10 +9,17 @@
     mkdir $RUNIDRIS_DIR
     chmod 700 $RUNIDRIS_DIR
 fi
-TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`.js"
+
+OS=`uname -s`
+case $OS in
+    OpenBSD ) TEMP_NAME="runidris-`sha1 -q $1`" ;;
+          * ) TEMP_NAME="runidris-`sha1sum $1 | cut -c1-40`" ;;
+esac
+
 FP="$RUNIDRIS_DIR/$TEMP_NAME"
-if [ ! -e $FP ]; then
-    "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." $1 -o $FP
+cp "$1" "$FP.idr" # idris won't compile the script unless it ends in .idr
+if [ ! -e "$FP.js" ]; then
+    "${IDRIS:-idris}" --codegen node --ibcsubdir "$RUNIDRIS_DIR" -i "." "$FP.idr" -o "$FP.js"
 fi
 shift
-node "$FP" "$@"
+node "$FP.js" "$@"
diff --git a/src/IRTS/CodegenC.hs b/src/IRTS/CodegenC.hs
--- a/src/IRTS/CodegenC.hs
+++ b/src/IRTS/CodegenC.hs
@@ -9,7 +9,7 @@
 
 module IRTS.CodegenC (codegenC) where
 
-import Idris.AbsSyntax hiding (getBC)
+import Idris.AbsSyntax
 import Idris.Core.TT
 import IRTS.Bytecode
 import IRTS.CodegenCommon
@@ -21,12 +21,10 @@
 import Util.System
 
 import Control.Monad
-import Control.Monad
-import Control.Monad.RWS
 import Data.Bits
 import Data.Char
-import Data.List (find, intercalate, nubBy, partition)
-import qualified Data.Text as T
+import Data.List (intercalate, nubBy)
+import Debug.Trace
 import Numeric
 import System.Directory
 import System.Exit
@@ -34,8 +32,6 @@
 import System.IO
 import System.Process
 
-import Debug.Trace
-
 codegenC :: CodeGenerator
 codegenC ci = do codegenC' (simpleDecls ci)
                            (outputFile ci)
@@ -70,9 +66,7 @@
          let bc = map toBC defs
          let wrappers = genWrappers bc
          let h = concatMap toDecl (map fst bc)
-         let (state, cc) = execRWS (generateSrc bc) 0
-                                         (CS { fnName = Nothing,
-                                                level = 1 })
+         let cc = concatMap (uncurry toC) bc
          let hi = concatMap ifaceC (concatMap getExp exports)
          d <- getIdrisCRTSDir
          mprog <- readFile (d </> "idris_main" <.> "c")
@@ -142,17 +136,12 @@
 toDecl :: Name -> String
 toDecl f = "void " ++ cname f ++ "(VM*, VAL*);\n"
 
-generateSrc :: [(Name, [BC])] -> RWS Int String CState ()
-generateSrc bc = mapM_ toC bc
-
-toC :: (Name, [BC]) -> RWS Int String CState ()
-toC (f, code) = do
-    modify (\s -> s { fnName = Just f })
-    s <- get
-    tell $ "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n"
-    tell $  indent (level s) ++ "INITFRAME;\n"
-    bcc code
-    tell $ "}\n\n"
+toC :: Name -> [BC] -> String
+toC f code
+    = -- "/* " ++ show code ++ "*/\n\n" ++
+      "void " ++ cname f ++ "(VM* vm, VAL* oldbase) {\n" ++
+                 indent 1 ++ "INITFRAME;\n" ++
+                 concatMap (bcc 1) code ++ "}\n\n"
 
 showCStr :: String -> String
 showCStr s = '"' : foldr ((++) . showChar) "\"" s
@@ -188,27 +177,15 @@
                  2 -> s
                  _ -> error $ "Can't happen: String of invalid length " ++ show s
 
-data CState = CS {
-    fnName :: Maybe Name,
-    level :: Int
-}
-
-
-bcc :: [BC] -> RWS Int String CState ()
-bcc [] = return ()
-bcc ((ASSIGN l r):xs) = do
-    i <- get
-    tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
-    bcc xs
-bcc ((ASSIGNCONST l c):xs) = do
-    i <- get
-    tell $ indent (level i) ++ creg l ++ " = " ++ mkConst c ++ ";\n"
-    bcc xs
+bcc :: Int -> BC -> String
+bcc i (ASSIGN l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
+bcc i (ASSIGNCONST l c)
+    = indent i ++ creg l ++ " = " ++ mkConst c ++ ";\n"
   where
     mkConst (I i) = "MKINT(" ++ show i ++ ")"
     mkConst (BI i) | i < (2^30) = "MKINT(" ++ show i ++ ")"
                    | otherwise = "MKBIGC(vm,\"" ++ show i ++ "\")"
-    mkConst (Fl f) = "MKFLOAT(vm, " ++ show f ++ ")"
+    mkConst (Fl f) = "MKFLOAT(vm, " ++ (map toUpper $ show f) ++ ")"
     mkConst (Ch c) = "MKINT(" ++ show (fromEnum c) ++ ")"
     mkConst (Str s) = "MKSTR(vm, " ++ showCStr s ++ ")"
     mkConst (B8  x) = "idris_b8const(vm, "  ++ show x ++ "U)"
@@ -221,21 +198,16 @@
     mkConst c | isTypeConst c = "MKINT(42424242)"
     mkConst c = error $ "mkConst of (" ++ show c ++ ") not implemented"
 
-bcc ((UPDATE l r):xs) = do
-    i <- get
-    tell $ indent (level i) ++ creg l ++ " = " ++ creg r ++ ";\n"
-    bcc xs
-bcc ((MKCON l loc tag []):xs) | tag < 256 = do
-    i <- get
-    tell $ indent (level i) ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
-    bcc xs
-bcc ((MKCON l loc tag args):xs) = do
-    i <- get
-    let tab = indent (level i)
-    tell $ tab ++ alloc loc tag ++
-           tab ++ setArgs 0 args ++ "\n" ++
-           tab ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
-    bcc xs
+bcc i (UPDATE l r) = indent i ++ creg l ++ " = " ++ creg r ++ ";\n"
+bcc i (MKCON l loc tag []) | tag < 256
+    = indent i ++ creg l ++ " = NULL_CON(" ++ show tag ++ ");\n"
+bcc i (MKCON l loc tag args)
+    = indent i ++ alloc loc tag ++
+      indent i ++ setArgs 0 args ++ "\n" ++
+      indent i ++ creg l ++ " = " ++ creg Tmp ++ ";\n"
+
+--         "MKCON(vm, " ++ creg l ++ ", " ++ show tag ++ ", " ++
+--         show (length args) ++ concatMap showArg args ++ ");\n"
   where showArg r = ", " ++ creg r
         setArgs i [] = ""
         setArgs i (x : xs) = "SETARG(" ++ creg Tmp ++ ", " ++ show i ++ ", " ++ creg x ++
@@ -247,94 +219,52 @@
             = "updateCon(" ++ creg Tmp ++ ", " ++ creg old ++ ", " ++ show tag ++ ", " ++
                     show (length args) ++ ");\n"
 
-bcc ((PROJECT l loc a):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "PROJECT(vm, " ++ creg l ++ ", "
-                ++ show loc ++ ", " ++ show a ++ ");\n"
-    bcc xs
-bcc ((PROJECTINTO r t idx):xs) = do
-    i <- get
-    tell $ indent (level i) ++ creg r ++ " = GETARG(" ++ creg t
-            ++ ", " ++ show idx ++ ");\n"
-    bcc xs
-bcc ((CASE True r code def):xs)
-    | length code < 4 = do
-        showCases def code
-        bcc xs
+bcc i (PROJECT l loc a) = indent i ++ "PROJECT(vm, " ++ creg l ++ ", " ++ show loc ++
+                                      ", " ++ show a ++ ");\n"
+bcc i (PROJECTINTO r t idx)
+    = indent i ++ creg r ++ " = GETARG(" ++ creg t ++ ", " ++ show idx ++ ");\n"
+bcc i (CASE True r code def)
+    | length code < 4 = showCase i def code
   where
-    showCode bc = do
-        w <- getBC bc xs
-        i <- get
-        tell $ "{\n" ++ w ++ indent (level i) ++ "}\n"
+    showCode :: Int -> [BC] -> String
+    showCode i bc = "{\n" ++ concatMap (bcc (i + 1)) bc ++
+                    indent i ++ "}\n"
 
-    showCases Nothing [(t, c)] = do
-        i <- get
-        tell $ indent (level i)
-        showCode c
-    showCases (Just def) [] = do
-        i <- get
-        tell $ indent (level i)
-        showCode def
-    showCases def ((t, c) : cs) = do
-        i <- get
-        tell $ indent (level i) ++ "if (CTAG(" ++ creg r ++ ") == "
-               ++ show t ++ ") "
-        showCode c
-        tell $ indent (level i) ++ "else\n"
-        showCases def cs
+    showCase :: Int -> Maybe [BC] -> [(Int, [BC])] -> String
+    showCase i Nothing [(t, c)] = indent i ++ showCode i c
+    showCase i (Just def) [] = indent i ++ showCode i def
+    showCase i def ((t, c) : cs)
+        = indent i ++ "if (CTAG(" ++ creg r ++ ") == " ++ show t ++ ") " ++ showCode i c
+           ++ indent i ++ "else\n" ++ showCase i def cs
 
-bcc ((CASE safe r code def):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n"
-    mapM showCase code
-    showDef def
-    tell $ indent (level i) ++ "}\n"
-    bcc xs
+bcc i (CASE safe r code def)
+    = indent i ++ "switch(" ++ ctag safe ++ "(" ++ creg r ++ ")) {\n" ++
+      concatMap (showCase i) code ++
+      showDef i def ++
+      indent i ++ "}\n"
   where
     ctag True = "CTAG"
     ctag False = "TAG"
 
-    showCase (t, bc) = do
-        w <- getBC bc xs
-        is <- get
-        let i = level is
-        tell $ indent i ++ "case " ++ show t ++ ":\n"
-                ++ w ++ indent (i + 1) ++ "break;\n"
-    showDef Nothing = return $ ()
-    showDef (Just c) = do
-        w <- getBC c xs
-        is <- get
-        let i = level is
-        tell $ indent i ++ "default:\n" ++ w ++ indent (i + 1) ++ "break;\n"
-
-bcc ((CONSTCASE r code def):xs)
+    showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
+                         ++ concatMap (bcc (i+1)) bc ++ indent (i + 1) ++ "break;\n"
+    showDef i Nothing = ""
+    showDef i (Just c) = indent i ++ "default:\n"
+                         ++ concatMap (bcc (i+1)) c ++ indent (i + 1) ++ "break;\n"
+bcc i (CONSTCASE r code def)
    | intConsts code
-     = do
-         is <- get
-         let i = level is
-         codes <- mapM getCode code
-         defs <- showDefS def
-         tell $ concatMap (iCase i (creg r)) codes
-         tell $ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
-         bcc xs
+--      = indent i ++ "switch(GETINT(" ++ creg r ++ ")) {\n" ++
+--        concatMap (showCase i) code ++
+--        showDef i def ++
+--        indent i ++ "}\n"
+     = concatMap (iCase (creg r)) code ++
+       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
    | strConsts code
-     = do
-         is <- get
-         let i = level is
-         codes <- mapM getCode code
-         defs <- showDefS def
-         tell $ concatMap (strCase i ("GETSTR(" ++ creg r ++ ")")) codes
-             ++ indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
-         bcc xs
+     = concatMap (strCase ("GETSTR(" ++ creg r ++ ")")) code ++
+       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
    | bigintConsts code
-     = do
-         is <- get
-         let i = level is
-         codes <- mapM getCode code
-         defs <- showDefS def
-         tell $ concatMap (biCase i (creg r)) codes ++
-            indent i ++ "{\n" ++ defs ++ indent i ++ "}\n"
-         bcc xs
+     = concatMap (biCase (creg r)) code ++
+       indent i ++ "{\n" ++ showDefS i def ++ indent i ++ "}\n"
    | otherwise = error $ "Can't happen: Can't compile const case " ++ show code
   where
     intConsts ((I _, _ ) : _) = True
@@ -351,118 +281,71 @@
     strConsts ((Str _, _ ) : _) = True
     strConsts _ = False
 
-    getCode (x, code) = do
-        c <- getBC code xs
-        return (x, c)
-
-    strCase i sv (s, bc) =
+    strCase sv (s, bc) =
         indent i ++ "if (strcmp(" ++ sv ++ ", " ++ show s ++ ") == 0) {\n" ++
-            bc ++ indent i ++ "} else\n"
-    biCase i bv (BI b, bc) =
+           concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    biCase bv (BI b, bc) =
         indent i ++ "if (bigEqConst(" ++ bv ++ ", " ++ show b ++ ")) {\n"
-           ++  bc ++ indent i ++ "} else\n"
-    iCase i v (I b, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (I b, bc) =
         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show b ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-    iCase i v (Ch b, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (Ch b, bc) =
         indent i ++ "if (GETINT(" ++ v ++ ") == " ++ show (fromEnum b) ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-    iCase i v (B8 w, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (B8 w, bc) =
         indent i ++ "if (GETBITS8(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-    iCase i v (B16 w, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (B16 w, bc) =
         indent i ++ "if (GETBITS16(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-    iCase i v (B32 w, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (B32 w, bc) =
         indent i ++ "if (GETBITS32(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-    iCase i v (B64 w, bc) =
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    iCase v (B64 w, bc) =
         indent i ++ "if (GETBITS64(" ++ v ++ ") == " ++ show (fromEnum w) ++ ") {\n"
-           ++ bc ++ indent i ++ "} else\n"
-
-    showDefS Nothing = return ""
-    showDefS (Just c) = getBC c xs
+           ++ concatMap (bcc (i+1)) bc ++ indent i ++ "} else\n"
+    showCase i (t, bc) = indent i ++ "case " ++ show t ++ ":\n"
+                         ++ concatMap (bcc (i+1)) bc ++
+                            indent (i + 1) ++ "break;\n"
+    showDef i Nothing = ""
+    showDef i (Just c) = indent i ++ "default:\n"
+                         ++ concatMap (bcc (i+1)) c ++
+                            indent (i + 1) ++ "break;\n"
+    showDefS i Nothing = ""
+    showDefS i (Just c) = concatMap (bcc (i+1)) c
 
-bcc (CALL n:xs) = do
-    i <- get
-    tell $ indent (level i) ++ "CALL(" ++ cname n ++ ");\n"
-    bcc xs
-bcc (TAILCALL n:xs) = do
-    i <- get
-    tell $ indent (level i) ++ "TAILCALL(" ++ cname n ++ ");\n"
-    bcc xs
-bcc ((SLIDE n):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "SLIDE(vm, " ++ show n ++ ");\n"
-    bcc xs
-bcc (REBASE:xs) = do
-    i <- get
-    tell $ indent (level i)++ "REBASE;\n"
-    bcc xs
-bcc ((RESERVE 0):xs) = bcc xs
-bcc ((RESERVE n):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "RESERVE(" ++ show n ++ ");\n"
-    bcc xs
-bcc ((ADDTOP 0):xs) = bcc xs
-bcc ((ADDTOP n):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "ADDTOP(" ++ show n ++ ");\n"
-    bcc xs
-bcc ((TOPBASE n):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "TOPBASE(" ++ show n ++ ");\n"
-    bcc xs
-bcc ((BASETOP n):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "BASETOP(" ++ show n ++ ");\n"
-    bcc xs
-bcc (STOREOLD:xs) = do
-    i <- get
-    tell $ indent (level i) ++ "STOREOLD;\n"
-    bcc xs
-bcc ((OP l fn args):xs) = do
-    i <- get
-    tell $ indent (level i) ++ doOp (creg l ++ " = ") fn args ++ ";\n"
-    bcc xs
-bcc ((FOREIGNCALL l rty (FStr fn@('&':name)) []):xs) = do
-    i <- get
-    tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
-    bcc xs
-bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%wrapper"
-      = do
-          i <- get
-          tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
+bcc i (CALL n) = indent i ++ "CALL(" ++ cname n ++ ");\n"
+bcc i (TAILCALL n) = indent i ++ "TAILCALL(" ++ cname n ++ ");\n"
+bcc i (SLIDE n) = indent i ++ "SLIDE(vm, " ++ show n ++ ");\n"
+bcc i REBASE = indent i ++ "REBASE;\n"
+bcc i (RESERVE 0) = ""
+bcc i (RESERVE n) = indent i ++ "RESERVE(" ++ show n ++ ");\n"
+bcc i (ADDTOP 0) = ""
+bcc i (ADDTOP n) = indent i ++ "ADDTOP(" ++ show n ++ ");\n"
+bcc i (TOPBASE n) = indent i ++ "TOPBASE(" ++ show n ++ ");\n"
+bcc i (BASETOP n) = indent i ++ "BASETOP(" ++ show n ++ ");\n"
+bcc i STOREOLD = indent i ++ "STOREOLD;\n"
+bcc i (OP l fn args) = indent i ++ doOp (creg l ++ " = ") fn args ++ ";\n"
+bcc i (FOREIGNCALL l rty (FStr fn@('&':name)) [])
+      = indent i ++
+        c_irts (toFType rty) (creg l ++ " = ") fn ++ ";\n"
+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%wrapper"
+      = indent i ++
+        c_irts (toFType rty) (creg l ++ " = ")
             ("_idris_get_wrapper(" ++ creg (snd x) ++ ")") ++ ";\n"
-          bcc zs
-bcc ((FOREIGNCALL l rty (FStr fn) (x:xs)):zs) | fn == "%dynamic"
-      = do
-          i <- get
-          tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
+bcc i (FOREIGNCALL l rty (FStr fn) (x:xs)) | fn == "%dynamic"
+      = indent i ++ c_irts (toFType rty) (creg l ++ " = ")
             ("(*(" ++ cFnSig "" rty xs ++ ") GETPTR(" ++ creg (snd x) ++ "))" ++
              "(" ++ showSep "," (map fcall xs) ++ ")") ++ ";\n"
-          bcc zs
-bcc ((FOREIGNCALL l rty (FStr fn) args):xs) = do
-    i <- get
-    tell $ indent (level i) ++ c_irts (toFType rty) (creg l ++ " = ")
-                 (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
-    bcc xs
-bcc ((FOREIGNCALL l rty _ args):_) = error "Foreign Function calls cannot be partially applied, without being inlined."
-bcc ((NULL r):xs) = do
-    i <- get
-    tell $ indent (level i) ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
-    bcc xs
-bcc ((ERROR str):xs) = do
-    i <- get
-    tell $ indent (level i) ++ "fprintf(stderr, "
-        ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
-    bcc xs
+bcc i (FOREIGNCALL l rty (FStr fn) args)
+      = indent i ++
+        c_irts (toFType rty) (creg l ++ " = ")
+                   (fn ++ "(" ++ showSep "," (map fcall args) ++ ")") ++ ";\n"
+bcc i (FOREIGNCALL l rty _ args) = error "Foreign Function calls cannot be partially applied, without being inlined."
+bcc i (NULL r) = indent i ++ creg r ++ " = NULL;\n" -- clear, so it'll be GCed
+bcc i (ERROR str) = indent i ++ "fprintf(stderr, " ++ show str ++ "); fprintf(stderr, \"\\n\"); exit(-1);\n"
 -- bcc i c = error (show c) -- indent i ++ "// not done yet\n"
-
-getBC code xs = do
-    i <- get
-    let (a, s, w) = runRWS (bcc code) 0 (i { level = level i + 1 })
-    return w
 
 fcall (t, arg) = irts_c (toFType t) (creg arg)
 -- Deconstruct the Foreign type in the defunctionalised expression and build
diff --git a/src/IRTS/Compiler.hs b/src/IRTS/Compiler.hs
--- a/src/IRTS/Compiler.hs
+++ b/src/IRTS/Compiler.hs
@@ -63,6 +63,8 @@
                              Nothing -> []
                              Just t -> freeNames t
 
+        logCodeGen 1 "Running Erasure Analysis"
+        iReport 3 "Running Erasure Analysis"
         reachableNames <- performUsageAnalysis
                               (rootNames ++ getExpNames exports)
         maindef <- case mtm of
diff --git a/src/Idris/Core/Binary.hs b/src/Idris/Core/Binary.hs
--- a/src/Idris/Core/Binary.hs
+++ b/src/Idris/Core/Binary.hs
@@ -16,6 +16,8 @@
 import Control.DeepSeq (($!!))
 import Control.Monad (liftM2)
 import Data.Binary
+import Data.Binary.Get
+import Data.Binary.Put
 import qualified Data.Text as T
 import qualified Data.Text.Encoding as E
 import Data.Vector.Binary
@@ -400,7 +402,7 @@
                 BI x1 -> do putWord8 1
                             put x1
                 Fl x1 -> do putWord8 2
-                            put x1
+                            putDoublele x1
                 Ch x1 -> do putWord8 3
                             put x1
                 Str x1 -> do putWord8 4
@@ -427,7 +429,7 @@
                            return (I x1)
                    1 -> do x1 <- get
                            return (BI x1)
-                   2 -> do x1 <- get
+                   2 -> do x1 <- getDoublele
                            return (Fl x1)
                    3 -> do x1 <- get
                            return (Ch x1)
diff --git a/src/Idris/DeepSeq.hs b/src/Idris/DeepSeq.hs
--- a/src/Idris/DeepSeq.hs
+++ b/src/Idris/DeepSeq.hs
@@ -29,20 +29,6 @@
 import Network.Socket (PortNumber)
 
 -- These types don't have Generic instances
-instance NFData CT.Options where
-  rnf (CT.Options x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()
-
-instance NFData CT.ListType where
-  rnf (CT.Bullet c) = rnf c `seq` ()
-  rnf (CT.Numbered nw i) = rnf nw `seq` rnf i `seq` ()
-
-instance NFData CT.CodeAttr where
-  rnf (CT.CodeAttr a b) = rnf a `seq` rnf b `seq` ()
-
-instance NFData CT.NumWrapper where
-  rnf CT.PeriodFollowing = ()
-  rnf CT.ParenFollowing = ()
-
 instance NFData DynamicLib where
     rnf (Lib x _) = rnf x `seq` ()
 
diff --git a/src/Idris/Erasure.hs b/src/Idris/Erasure.hs
--- a/src/Idris/Erasure.hs
+++ b/src/Idris/Erasure.hs
@@ -1,6 +1,6 @@
 {-|
 Module      : Idris.Erasure
-Description : Utilities to erase irrelevant stuff.
+Description : Utilities to erase stuff not necessary for runtime.
 Copyright   :
 License     : BSD3
 Maintainer  : The Idris Community.
@@ -145,10 +145,54 @@
         fmt n rs = show n ++ " from " ++ intercalate ", " [show rn ++ " arg# " ++ show ri | (rn,ri) <- rs]
         warn = logErasure 0
 
+type Constraint = (Cond, DepSet)
+
 -- | Find the minimal consistent usage by forward chaining.
+--
+-- We use a cleverer implementation that:
+-- 1. First transforms Deps into a collection of numbered constraints
+-- 2. For each node, we remember the numbers of constraints
+--    that contain that node among their preconditions.
+-- 3. When performing forward chaining, we perform unit propagation
+--    only on the relevant constraints, not all constraints.
+--
+-- Typical numbers from the current version of Blodwen:
+-- * 56 iterations until fixpoint
+-- * out of 20k constraints total, 5-1000 are relevant per iteration
 minimalUsage :: Deps -> (Deps, (Set Name, UseMap))
-minimalUsage = second gather . forwardChain
+minimalUsage deps
+    = fromNumbered *** gather
+    $ forwardChain (index numbered) seedDeps seedDeps numbered
   where
+    numbered = toNumbered deps
+
+    -- The initial solution. Consists of nodes that are
+    -- reachable immediately, without any preconditions.
+    seedDeps :: DepSet
+    seedDeps = M.unionsWith S.union [ds | (cond, ds) <- IM.elems numbered, S.null cond]
+
+    toNumbered :: Deps -> IntMap Constraint
+    toNumbered = IM.fromList . zip [0..] . M.toList
+
+    fromNumbered :: IntMap Constraint -> Deps
+    fromNumbered = IM.foldr addConstraint M.empty
+      where
+        addConstraint (ns, vs) = M.insertWith (M.unionWith S.union) ns vs
+
+    -- Build an index that maps every node to the set of constraints
+    -- where the node appears among the preconditions.
+    index :: IntMap Constraint -> Map Node IntSet
+    index = IM.foldrWithKey (
+            -- for each clause (i. ns --> _ds)
+            \i (ns, _ds) ix -> foldr (
+                -- for each node `n` in `ns`
+                \n ix' -> M.insertWith IS.union n (IS.singleton i) ix'
+              ) ix (S.toList ns)
+        ) M.empty
+
+    -- Convert a solution of constraints into:
+    -- 1. the list of names used in the program
+    -- 2. the list of arguments used, together with their reasons
     gather :: DepSet -> (Set Name, UseMap)
     gather = foldr ins (S.empty, M.empty) . M.toList
        where
@@ -156,17 +200,81 @@
         ins ((n, Result), rs) (ns, umap) = (S.insert n ns, umap)
         ins ((n, Arg i ), rs) (ns, umap) = (ns, M.insertWith (IM.unionWith S.union) n (IM.singleton i rs) umap)
 
-forwardChain :: Deps -> (Deps, DepSet)
-forwardChain deps
-    | Just trivials <- M.lookup S.empty deps
-        = (M.unionWith S.union trivials)
-            `second` forwardChain (remove trivials . M.delete S.empty $ deps)
-    | otherwise = (deps, M.empty)
+-- | In each iteration, we find the set of nodes immediately reachable
+-- from the current set of constraints, and then reduce the set of constraints
+-- based on that knowledge.
+--
+-- In the implementation, this is phase-shifted. We first reduce the set
+-- of constraints, given the newly reachable nodes from the previous iteration,
+-- and then compute the set of currently reachable nodes.
+-- Then we decide whether to iterate further.
+forwardChain
+    :: Map Node IntSet   -- ^ node index
+    -> DepSet            -- ^ all reachable nodes found so far
+    -> DepSet            -- ^ nodes reached in the previous iteration
+    -> IntMap Constraint -- ^ numbered constraints
+    -> (IntMap Constraint, DepSet)
+forwardChain index solution previouslyNew constrs
+    -- no newly reachable nodes, fixed point has been reached
+    | M.null currentlyNew
+    = (constrs, solution)
+
+    -- some newly reachable nodes, iterate more
+    | otherwise
+    = forwardChain index
+        (M.unionWith S.union solution currentlyNew)
+        currentlyNew
+        constrs'
   where
-    -- Remove the given nodes from the Deps entirely,
-    -- possibly creating new empty Conds.
-    remove :: DepSet -> Deps -> Deps
-    remove ds = M.mapKeysWith (M.unionWith S.union) (S.\\ M.keysSet ds)
+    -- which constraints could give new results,
+    -- given that `previouslyNew` has been derived in the last iteration
+    affectedIxs = IS.unions [
+        M.findWithDefault IS.empty n index
+        | n <- M.keys previouslyNew
+      ]
+
+    -- traverse all (potentially) affected constraints, building:
+    -- 1. a set of newly reached nodes
+    -- 2. updated set of constraints where the previously
+    --    reached nodes have been removed
+    (currentlyNew, constrs')
+        = IS.foldr
+            (reduceConstraint $ M.keysSet previouslyNew)
+            (M.empty, constrs)
+            affectedIxs
+
+    -- Update the pair (newly reached nodes, numbered constraint set)
+    -- by reducing the constraint with the given number.
+    reduceConstraint
+        :: Set Node  -- ^ nodes reached in the previous iteration
+        -> Int       -- ^ constraint number
+        -> (DepSet, IntMap (Cond, DepSet))
+        -> (DepSet, IntMap (Cond, DepSet))
+    reduceConstraint previouslyNew i (news, constrs)
+        | Just (cond, deps) <- IM.lookup i constrs
+        = case cond S.\\ previouslyNew of
+            cond'
+                -- This constraint's set of preconditions has shrunk
+                -- to the empty set. We can add its RHS to the set of newly
+                -- reached nodes, and remove the constraint altogether.
+                | S.null cond'
+                -> (M.unionWith S.union news deps, IM.delete i constrs)
+
+                -- This constraint's set of preconditions has shrunk
+                -- so we need to overwrite the numbered slot
+                -- with the updated constraint.
+                | S.size cond' < S.size cond
+                -> (news, IM.insert i (cond', deps) constrs)
+
+                -- This constraint's set of preconditions hasn't changed
+                -- so we do not do anything about it.
+                | otherwise
+                -> (news, constrs)
+
+        -- Constraint number present in index but not found
+        -- among the constraints. This happens more and more frequently
+        -- as we delete constraints from the set.
+        | otherwise = (news, constrs)
 
 -- | Build the dependency graph, starting the depth-first search from
 -- a list of Names.
diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs
--- a/src/Idris/IBC.hs
+++ b/src/Idris/IBC.hs
@@ -48,7 +48,7 @@
 import System.FilePath
 
 ibcVersion :: Word16
-ibcVersion = 161
+ibcVersion = 162
 
 -- | When IBC is being loaded - we'll load different things (and omit
 -- different structures/definitions) depending on which phase we're in.
diff --git a/stack.yaml b/stack.yaml
--- a/stack.yaml
+++ b/stack.yaml
@@ -1,3 +1,4 @@
+#recheck extra-deps next on resolver or cabal file change
 resolver: lts-9.0
 
 packages:
@@ -9,7 +10,8 @@
     GMP: true
 
 extra-deps:
-  - libffi-0.1
+  - binary-0.8.5.1
+  - cheapskate-0.1.1
 
 nix:
   enable: false
diff --git a/test/TestRun.hs b/test/TestRun.hs
--- a/test/TestRun.hs
+++ b/test/TestRun.hs
@@ -65,7 +65,8 @@
   where
     ref = path </> "expected"
     output = path </> "output"
-    diff ref new = ["diff", "--strip-trailing-cr", "-u", new, ref]
+    diff ref new | os == "openbsd" = ["diff", "-u", new, ref]
+                 | otherwise = ["diff", "--strip-trailing-cr", "-u", new, ref]
 
 -- Should always output a 3-charater string from a postive Int
 indexToString :: Int -> String
diff --git a/test/base001/exit1.c b/test/base001/exit1.c
--- a/test/base001/exit1.c
+++ b/test/base001/exit1.c
@@ -1,6 +1,10 @@
 #include <stdio.h>
 #include <stdlib.h>
 
+#ifdef __OpenBSD__
+#include <sys/wait.h>
+#endif
+
 void doSystem(const char cmd[]) {
   printf("exit1: Executing cmd '%s'\n", cmd);
   int exitStatus = system(cmd);
diff --git a/test/base001/sys.c b/test/base001/sys.c
--- a/test/base001/sys.c
+++ b/test/base001/sys.c
@@ -2,6 +2,10 @@
 
 #include <stdlib.h>
 
+#ifdef __OpenBSD__
+#include <sys/wait.h>
+#endif
+
 int WIFEXITED_(int status) {
   return WIFEXITED(status);
 }