diff --git a/CHANGELOG b/CHANGELOG
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -1,5 +1,7 @@
 CHANGELOG for MiniAgda
 
+0.2025.7.23   Drop support for GHC 7, tested with GHC 8.0 - 9.12.2.
+
 0.2022.3.11   Fixed compilation with mtl-2.3-rc3, tested with ghc 9.2.2, added cabal test.
 
 0.2020.4.14   Tested compilation with ghc 8.10.1.
diff --git a/MiniAgda.cabal b/MiniAgda.cabal
--- a/MiniAgda.cabal
+++ b/MiniAgda.cabal
@@ -1,6 +1,7 @@
 cabal-version:   2.4
+  -- 2.4 introduces the ** glob patterns used in data-files
 name:            MiniAgda
-version:         0.2022.3.11
+version:         0.2025.7.23
 build-type:      Simple
 license:         MIT
 license-file:    LICENSE
@@ -23,7 +24,12 @@
   patterns for a more general handling of coinduction.
 
 tested-with:
-  GHC == 9.2.2
+  GHC == 9.12.2
+  GHC == 9.10.2
+  GHC == 9.8.4
+  GHC == 9.6.7
+  GHC == 9.4.8
+  GHC == 9.2.8
   GHC == 9.0.2
   GHC == 8.10.7
   GHC == 8.8.4
@@ -31,15 +37,22 @@
   GHC == 8.4.4
   GHC == 8.2.2
   GHC == 8.0.2
-  GHC == 7.10.3
-  GHC == 7.8.4
-  GHC == 7.6.3
 
-extra-source-files:
+extra-doc-files:
   CHANGELOG
   README.md
+
+extra-source-files:
   Makefile
   src/Makefile
+  stack-9.12.yaml
+  stack-9.10.yaml
+  stack-9.8.yaml
+  stack-9.6.yaml
+  stack-9.4.3.yaml
+  stack-9.2.5.yaml
+  stack-9.0.2.yaml
+  stack-8.10.7.yaml
 
 data-files:
   test/fail/Makefile
@@ -54,19 +67,25 @@
   type:     git
   location: https://github.com/andreasabel/miniagda
 
-executable miniagda
+library
   hs-source-dirs:       src
   build-depends:        array             >= 0.3    && < 0.6
-                      , base              >= 4.6    && < 5
-                      , containers        >= 0.3    && < 0.7
+                      , base              >= 4.9    && < 5
+                      , containers        >= 0.3    && < 1
                       , haskell-src-exts  >= 1.21   && < 1.22
                           -- haskell-src-exts is a nervous package with incompatibilities
                           -- in every new version, thus, we need tight bounds.
-                      , mtl               >= 2.2.2  && < 2.4
+                      , mtl               >= 2.2.1  && < 2.4
+                      , optparse-applicative
+                                          >= 0.16.0.0 && < 1
+                          -- optparse-applicative-0.16.0.0 adds some1
                       , pretty            >= 1.0    && < 1.2
+                      , string-qq
                       , transformers
-  build-tool-depends:   happy:happy       >= 1.15   && < 2
+
+  build-tool-depends:   happy:happy       >= 1.15   && < 3
                       , alex:alex         >= 3.0    && < 4
+
   default-language:     Haskell98
   default-extensions:   CPP
                         MultiParamTypeClasses
@@ -79,14 +98,17 @@
                         TupleSections
                         NamedFieldPuns
                         LambdaCase
-  main-is:              Main.hs
-  other-modules:        Abstract
+
+  exposed-modules:      Abstract
                         Collection
                         Concrete
                         Eval
                         Extract
                         HsSyntax
                         Lexer
+                        License
+                        MainLib
+                        Options
                         Parser
                         Polarity
                         PrettyTCM
@@ -96,27 +118,33 @@
                         TCM
                         Termination
                         ToHaskell
-                        Tokens
                         TraceError
                         TreeShapedOrder
                         TypeChecker
                         Util
                         Value
+                        Version
                         Warshall
+  other-modules:        Paths_MiniAgda
+  autogen-modules:      Paths_MiniAgda
 
-  -- TODO: Warning-free
-  -- ghc-options:      -Wall
-  --                   -fno-warn-type-defaults
-  --                   -fno-warn-dodgy-imports
-  --                   -fno-warn-unused-binds
-  --                   -fno-warn-unused-matches
-  --                   -fno-warn-name-shadowing
-  --                   -fno-warn-incomplete-patterns
+  ghc-options:          -Wall
+                        -Wcompat
+                        -Wno-type-defaults
+                        -Wno-dodgy-imports
+                        -Wno-unused-binds
+                        -Wno-unused-matches
+                        -Wno-name-shadowing
+                        -Wno-incomplete-patterns
 
-  if impl(ghc >= 8.0)
-    ghc-options:        -Wcompat
   if impl(ghc >= 9.2)
     ghc-options:        -Wno-incomplete-uni-patterns
+                        -Wno-incomplete-record-updates
+executable miniagda
+  hs-source-dirs:       main
+  main-is:              Main.hs
+  build-depends:        MiniAgda
+  default-language:     Haskell2010
 
 test-suite test
   type:                 exitcode-stdio-1.0
@@ -124,7 +152,7 @@
   main-is:              GoldplateTests.hs
   default-language:     Haskell2010
   ghc-options:          -threaded
-  build-depends:        base >= 4.11
+  build-depends:        base >= 4.11 && < 5
                           -- goldplate requires ghc >= 8.4
                       , process
   build-tool-depends:   goldplate:goldplate >= 0.2
diff --git a/README.md b/README.md
--- a/README.md
+++ b/README.md
@@ -10,7 +10,7 @@
 
 A prototypical dependently typed languages with sized types and variances.
 
-## Installation
+## Installation from Hackage
 
 Requires `ghc` and `cabal`, for instance via the Haskell Platform or via `ghcup`.
 In a shell, type
@@ -19,11 +19,63 @@
   cabal install MiniAgda
 ```
 
-To build MiniAgda from source, replace the last command with
+## Installation from Stackage
 
-```
- make
-```
+MiniAgda is not on Stackage because it depends on a specific version of `haskell-src-exts` rather than the latest version.
+You can install with `stack` from source though, see next section.
+
+## Installation from source
+
+1. Obtain the sources.
+   ```
+   git clone https://github.com/andreasabel/miniagda
+   cd miniagda
+   ```
+
+2. Checkout the desired version (optional):
+   If you want to build a released version or a branch rather than the latest `master`, switch to this version/branch.
+   ```
+   git checkout $REF
+   ```
+   E.g. `REF = v0.2022.3.11` for version `0.2022.3.11` or `REF = unfold` for branch `unfold`.
+
+3. Building and running the tests (optional).
+
+   - With `cabal` (requires `ghc` in your PATH):
+     ```
+     cabal build --enable-tests
+     cabal test
+     ```
+     After building, you can run MiniAgda locally, e.g.:
+     ```
+     cabal run miniagda -- examples/Gcd/gcd.ma
+     ```
+
+   - With `stack`:
+     ```
+     stack build --stack-yaml=stack-$GHCVER.yaml
+     stack test  --stack-yaml=stack-$GHCVER.yaml
+     ```
+     At the time of writing (2025-07-23), `GHCVER` can be any of `9.12`, `9.10`, `9.8`, `9.6`, and some older ones.
+
+     After building, you can run MiniAgda locally, e.g.:
+     ```
+     stack run --stack-yaml=stack-9.12.yaml -- examples/Gcd/gcd.ma
+     ```
+     You can copy `stack-$GHCVER.yaml` for your choice of `GHCVER` into `stack.yaml` and drop the `--stack-yaml` argument from `stack` invocation.
+
+
+4. Install.
+   - With `cabal` (requires `ghc` in your PATH):
+     ```
+     cabal install
+     ```
+   - With `stack`:
+     ```
+     stack install --stack-yaml=stack-$GHCVER.yaml
+     ```
+
+   Note that the respective installation directory should be on your PATH.
 
 ## Examples
 
diff --git a/main/Main.hs b/main/Main.hs
new file mode 100644
--- /dev/null
+++ b/main/Main.hs
@@ -0,0 +1,5 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Main (module X) where
+
+import MainLib as X (main)
diff --git a/src/Abstract.hs b/src/Abstract.hs
--- a/src/Abstract.hs
+++ b/src/Abstract.hs
@@ -13,14 +13,15 @@
 import Prelude hiding (showList, map, concat, foldl, pi, null, (<>))
 
 #if !MIN_VERSION_base(4,8,0)
-import Control.Applicative hiding (empty)
+import Control.Applicative (Applicative, pure, (<*>), (<$>))
 #endif
 import Control.Monad.Writer (Writer, tell)
 import Control.Monad.Trans
 
 import Control.Arrow (first)
-import Data.Monoid hiding ((<>))
+import Data.Monoid (All(..))
 #if !MIN_VERSION_base(4,8,0)
+import Data.Monoid (mempty, mconcat)
 import Data.Foldable (Foldable, foldMap)
 import Data.Traversable (Traversable)
 #endif
@@ -220,6 +221,7 @@
 paramDec = Dec Param
 defaultDec = Dec defaultPol
 -- defaultDec = paramDec -- TODO: Dec { polarity = Rec }
+
 defaultUpperDec :: Decoration PProd
 defaultUpperDec = Dec $ pprod SPos
   -- a variable may not be erased and its polarity must be below SPos
@@ -338,17 +340,15 @@
 leqSizeE (Succ e) (Succ e') = leqSizeE e e'
 leqSizeE Infty _ = False
 
--- plus :: Expr -> Expr -> Expr
-
 -- sorts -------------------------------------------------------------
 
 data Class
   = Tm      -- sort of terms, only needed for erasure
---  | Ty    -- use Set 0!  -- sort of type(constructor)s, only needed for erasure
---  | Ki      -- sort of kinds  -- use Set 0 ... for mor precision
+  -- -- | Ty    -- use Set 0!  -- sort of type(constructor)s, only needed for erasure
+  -- -- | Ki      -- sort of kinds  -- use Set 0 ... for mor precision
   | Size    -- sort of sizes
   | TSize   -- sort of Size
-  -- | Type    -- no longer used
+  -- -- | Type    -- no longer used
     deriving (Eq, Ord, Show)
 
 predClass :: Class -> Class
@@ -371,11 +371,11 @@
 -}
 
 instance Show (Sort Expr) where
-  show (SortC c) = show c
-  show (Set Zero) = "Set"
+  show (SortC c)     = show c
+  show (Set Zero)    = "Set"
   show (CoSet Infty) = "Set"
-  show (Set e) = Util.parens $ ("Set " ++ show e)
-  show (CoSet e) = Util.parens $ ("CoSet " ++ show e)
+  show (Set e)       = Util.parens $ ("Set " ++ show e)
+  show (CoSet e)     = Util.parens $ ("CoSet " ++ show e)
 
 topSort :: Sort Expr
 topSort = Set Infty
@@ -421,8 +421,8 @@
 minClass Size _ = Size
 minClass _ Size = Size
 minClass TSize TSize = TSize
-maxClass :: Class -> Class -> Class
 
+maxClass :: Class -> Class -> Class
 maxClass Tm c = c
 maxClass c Tm = c
 maxClass Size c = c
@@ -444,7 +444,7 @@
 leSort s s'   = s == s'
 -}
 
--- s `irrSortFor` s' if a variable of kind s cannot compuationally
+-- s `irrSortFor` s' if a variable of kind s cannot computationally
 -- contribute to produce a value of kind s'
 irrSortFor :: Sort Expr -> Sort Expr -> Bool
 irrSortFor (SortC Tm) _          = False -- terms matter for terms and everything
@@ -604,15 +604,6 @@
   getPol = getPol . getDec
   mapPol = mapDec . mapPol
 
-{-
-instance Functor Dom where
-  fmap f dom = dom { typ = f (typ dom) }
-
--- traverse :: Applicative f => (a -> f b) -> t a -> f (t b)
-instance Traversable Dom where
-  traverse f dom = (\ ty -> dom { typ = ty }) <$> f (typ dom)
--}
-
 -- identifiers -------------------------------------------------------
 
 -- |
@@ -943,7 +934,7 @@
   The whole pattern is not irrefutable, but still you want the pair destructed
   lazily by projections.
 -}
---  | IrrP -- pattern which got erased
+-- --  | IrrP -- pattern which got erased
                deriving (Eq,Ord)
 
 {-
@@ -1846,7 +1837,7 @@
     (Var name            , []) -> Set.singleton name
     (Def (DefId DatK{} _), es) -> injectiveVars es
     (Def (DefId ConK{} _), es) -> injectiveVars es
-    (Record ri rs        , []) -> Set.unions $ List.map (injectiveVars . snd) rs
+    (Record _ri rs       , []) -> Set.unions $ List.map (injectiveVars . snd) rs
     (Succ e              , []) -> injectiveVars e
     (Lam _ x e           , []) -> Set.delete x (injectiveVars e)
     (Quant _ ta b , []) -> injectiveVars ta `Set.union` (injectiveVars b Set.\\ boundVars ta)
@@ -1858,7 +1849,7 @@
     _                         -> Set.empty
 
 classifyFields :: Co -> Name -> Type -> [FieldInfo]
-classifyFields co dataName ty = List.map (classifyField fvs) $ telescope tele
+classifyFields _co _19dataName ty = List.map (classifyField fvs) $ telescope tele
   where (tele, core) = typeToTele ty
         fvs = freeVars core
         ivs = injectiveVars core
@@ -1975,7 +1966,7 @@
 reassembleConstructorType ci = buildPi (cFields ci) where
   buildPi [] = cTyCore ci
   buildPi (f:fs) = pi (TBind (fName f) $ Domain (fType f) defaultKind (decor (fDec f) (fClass f))) $ buildPi fs
-    where decor dec Index = irrelevantDec -- DONE: SWITCH ON!
+    where decor _   Index = irrelevantDec -- DONE: SWITCH ON!
           decor dec _     = dec
 
 -- Pattern inductive families ----------------------------------------
@@ -1997,7 +1988,7 @@
 --   Gamma -> D ps
 -- and returns the list ps of patterns if it is the case
 isPatIndFamC :: Expr -> Writer All [Pattern]
-isPatIndFamC (Def id) = return []
+isPatIndFamC (Def _) = return []
 isPatIndFamC (App f e) = do
   ps <- isPatIndFamC f
   p  <- exprToDotPat' e
@@ -2015,30 +2006,30 @@
 -- TreeShapedOrder
 tsoFromPatterns :: [Pattern] -> TSO Name
 tsoFromPatterns ps = TSO.fromList $ List.concat $ List.map loop ps where
-  loop (SizeP (Var father) son) = [(son,(1,father))]
+  loop (SizeP (Var father) son)        = [(son,(1,father))]
   loop (SizeP (Succ (Var father)) son) = [(son,(0,father))]
-  loop (SizeP e      son) = []
-  loop (ConP _ _ ps)      = List.concat $ List.map loop ps
-  loop (PairP p p')       = loop p ++ loop p'
-  loop (SuccP   p)        = loop p
-  loop (ErasedP p)        = loop p
-  loop ProjP{}            = []
-  loop VarP{}             = []
-  loop DotP{}             = []
-  loop UnusableP{}        = []
+  loop (SizeP{})                       = []
+  loop (ConP _ _ ps)                   = List.concat $ List.map loop ps
+  loop (PairP p p')                    = loop p ++ loop p'
+  loop (SuccP   p)                     = loop p
+  loop (ErasedP p)                     = loop p
+  loop ProjP{}                         = []
+  loop VarP{}                          = []
+  loop DotP{}                          = []
+  loop UnusableP{}                     = []
 
 -- for non-dot patterns, patterns overlap if one matches against the other
 -- infinity size is represented as (DotP Infty)
 -- I reprogram it here, since it does not need a monad
 overlap :: Pattern -> Pattern -> Bool
-overlap (VarP _) p' = True
-overlap p (VarP _)  = True
+overlap (VarP _) _ = True
+overlap _ (VarP _) = True
 overlap (ConP _ c ps) (ConP _ c' ps') = c == c' && overlaps ps ps' -- only source of non-overlap
 overlap (PairP p1 p2) (PairP p1' p2') = overlaps [p1,p2] [p1',p2']
 overlap (ProjP n) (ProjP n') = n == n' -- another source of non-overlap
 -- size patterns always overlap
-overlap (SuccP p) _ = True
-overlap _ (SuccP p) = True
+overlap (SuccP _) _ = True
+overlap _ (SuccP _) = True
 overlap SizeP{} _   = True
 overlap _ SizeP{}   = True
 -- dot patterns always overlap (safe approximation)
@@ -2103,7 +2094,7 @@
 
 patternToExpr :: Pattern -> Expr
 patternToExpr (VarP n)       = Var n
-patternToExpr (SizeP m n)    = Var n
+patternToExpr (SizeP _m n)   = Var n
 patternToExpr (ConP pi n ps) = List.foldl App (con (coPat pi) n) (List.map patternToExpr ps)
 -- patternToExpr (ConP co n ps) = Con co n `App` (List.map patternToExpr ps)
 patternToExpr (PairP p p')   = Pair (patternToExpr p) (patternToExpr p')
@@ -2146,7 +2137,7 @@
 
 isSuccessor :: Expr -> Bool
 isSuccessor (Ann e)  = isSuccessor (unTag e)
-isSuccessor (Succ e) = True
+isSuccessor (Succ _) = True
 isSuccessor _        = False
 
 shallowSuccP :: Pattern -> Bool
@@ -2186,7 +2177,7 @@
       ttt :: Int -> Type -> [TBind] -> ([TBind], Type)
 --      ttt k (Quant Pi htel tb t2) tel | k /= 0 = ttt (k-1) t2 (telescope htel ++ tb : tel)
       ttt k (Quant Pi tb t2) tel | k /= 0 = ttt (k-1) t2 (tb : tel)
-      ttt k t tel = (reverse tel, t)
+      ttt _ t tel = (reverse tel, t)
 
 ---- modification
 
diff --git a/src/Concrete.hs b/src/Concrete.hs
--- a/src/Concrete.hs
+++ b/src/Concrete.hs
@@ -5,13 +5,13 @@
 import Prelude hiding (null)
 
 import Util
-import Abstract (Co,Sized,PiSigma(..),Decoration(..),Dec,Override(..),Measure(..),Bound(..),HasPred(..),LtLe(..),polarity)
-import qualified Abstract as A
+import Abstract
+  (Co, Sized, PiSigma(..), Dec, Override(..), Measure(..), Bound(..), HasPred(..), LtLe(..), polarity)
 import Polarity
 
 -- | Concrete names.
 data Name = Name { theName :: String }
-  deriving (Eq,Ord)
+  deriving (Eq, Ord)
 
 instance Show Name where
   show (Name n) = n
@@ -20,15 +20,19 @@
 data QName
   = Qual  { qual :: Name, name :: Name }  -- ^ @X.x@ e.g. qualified constructor.
   | QName { name :: Name }                -- ^ @x@.
-  deriving (Eq,Ord)
+  deriving (Eq, Ord)
 
+unqual :: QName -> Name
 unqual (QName n) = n
 
 instance Show QName where
   show (Qual m n) = show m ++ "." ++ show n
   show (QName n)  = show n
 
+set0 :: Expr
 set0 = Set Zero
+
+ident :: Name -> Expr
 ident n = Ident (QName n)
 
 -- | Concrete expressions syntax.
@@ -236,6 +240,7 @@
 prettyTel :: Bool -> Telescope -> String
 prettyTel inPi = Util.showList " " (prettyTBind inPi)
 
+prettyMaybeType :: Maybe Expr -> String
 prettyMaybeType = maybe "" $ \ t -> " : " ++ prettyExpr t
 
 prettyExpr :: Expr -> String
@@ -269,8 +274,10 @@
       Quant pisig tel t2 -> parens $ prettyTel True tel
                                   ++ " " ++ show pisig ++ " " ++ prettyExpr t2
 
+prettyRecordLine :: ([Name], Expr) -> String
 prettyRecordLine (xs, e) = Util.showList " " show xs ++ " = " ++ prettyExpr e
 
+prettyCase :: Clause -> String
 prettyCase (Clause Nothing [p] Nothing)  = prettyPattern p
 prettyCase (Clause Nothing [p] (Just e)) = prettyPattern p ++ " -> " ++ prettyExpr e
 
@@ -287,6 +294,7 @@
 prettyExprs :: [Expr] -> String
 prettyExprs = Util.showList " " prettyExpr
 
+prettyDecl :: Declaration -> String
 prettyDecl (PatternDecl n ns p) = "pattern " ++ (Util.showList " " show (n:ns)) ++ " = " ++ prettyPattern p
 
 teleToType :: Telescope -> Type -> Type
diff --git a/src/Eval.hs b/src/Eval.hs
--- a/src/Eval.hs
+++ b/src/Eval.hs
@@ -2,6 +2,8 @@
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE CPP #-}
 
+{-# OPTIONS_GHC -fno-warn-orphans #-}
+
 -- Activate this flag if i < $i should only hold for i < #.
 -- #define STRICTINFTY
 
@@ -9,24 +11,25 @@
 
 import Prelude hiding (mapM, null, pi)
 
+#if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
+#endif
 import Control.Monad          hiding (mapM)
 import Control.Monad.State    (StateT, execStateT, get, gets, put)
 import Control.Monad.Except   (runExcept, MonadError)
 import Control.Monad.Reader   (asks, local)
 
 import qualified Data.Array as Array
-import Data.Maybe -- fromMaybe
-import Data.Monoid hiding ((<>))
-import Data.List (find)
 import qualified Data.List as List
-import Data.Map (Map)
 import qualified Data.Map as Map
+#if !MIN_VERSION_base(4,8,0)
 import Data.Foldable (foldMap)
-import Data.Traversable (Traversable, mapM, traverse)
-import qualified Data.Traversable as Traversable
+import Data.Monoid
+import Data.Traversable (traverse)
+#endif
+import Data.Traversable (mapM)
 
-import Debug.Trace (trace)
+-- import Debug.Trace (trace)
 
 import Abstract
 import Polarity as Pol
@@ -39,6 +42,8 @@
 import TraceError
 import Util
 
+traceEta, traceRecord, traceMatch, traceLoop, traceSize :: String -> a -> a
+traceEtaM, traceRecordM, traceMatchM, traceLoopM, traceSizeM :: Monad m => String -> m ()
 
 traceEta msg a = a -- trace msg a
 traceEtaM msg = return () -- traceM msg
@@ -114,7 +119,7 @@
   reval = reval' emptyVal
 
 instance Reval a => Reval (Maybe a) where
-  reval' valu ma = Traversable.traverse (reval' valu) ma
+  reval' valu ma = traverse (reval' valu) ma
 
 instance Reval b => Reval (a,b) where
   reval' valu (x,v) = (x,) <$> reval' valu v
@@ -134,10 +139,10 @@
     reval' valu valu'
 
 instance Reval a => Reval (Measure a) where
-  reval' valu beta = Traversable.traverse (reval' valu) beta
+  reval' valu beta = traverse (reval' valu) beta
 
 instance Reval a => Reval (Bound a) where
-  reval' valu beta = Traversable.traverse (reval' valu) beta
+  reval' valu beta = traverse (reval' valu) beta
 
 instance Reval Val where
   reval' valu u = traceLoop ("reval " ++ show u) $ do
@@ -177,11 +182,11 @@
       VGuard beta v         -> VGuard <$> reval beta <*> reval v
       VQuant pisig x dom fv ->
         VQuant pisig x
-          <$> Traversable.mapM reval dom
+          <$> mapM reval dom
           <*> reFun fv
     {-
       VQuant pisig x dom env b -> do
-        dom' <- Traversable.mapM reval dom
+        dom' <- mapM reval dom
         env' <- reEnv env
         return $ VQuant pisig x dom' env' b
     -}
@@ -284,6 +289,7 @@
 equals' (w1:vs1) (w2:vs2) = (equal' w1 w2) `andLazy` (equals' vs1 vs2)
 equals' vl1 vl2           = return False
 
+equal' :: Val -> Val -> TypeCheck Bool
 equal' w1 w2 = whnfClos w1 >>= \ v1 -> equal v1 =<< whnfClos w2
 
 {- LEADS TO NON-TERMINATION
@@ -317,7 +323,7 @@
     (VSort s)            -> return $ Sort $ vSortToSort s
     (VBelow ltle v)      -> Below ltle <$> reify v
     (VQuant pisig x dom fv) -> do
-          dom' <- Traversable.mapM reify dom
+          dom' <- mapM reify dom
           underAbs_ x dom fv $ \ k xv vb -> do
             let x' = unsafeName (suggestion x ++ "~" ++ show k)
             piSig pisig (TBind x' dom') <$> reify vb
@@ -538,12 +544,12 @@
     Lam dec x e1 -> return $ vLam x env e1
     Below ltle e -> VBelow ltle <$> whnf env e
     Quant pisig (TBind x dom) b -> do
-      dom' <- Traversable.mapM (whnf env) dom  -- Pi is strict in its first argument
+      dom' <- mapM (whnf env) dom  -- Pi is strict in its first argument
       return $ VQuant pisig x dom' $ vLam x env b
 
     -- a measured type evaluates to
-    -- * a bounded type if measure present in environment (rhs of funs)
-    -- * otherwise to a measured type (lhs of funs)
+    -- - a bounded type if measure present in environment (rhs of funs)
+    -- - otherwise to a measured type (lhs of funs)
     Quant Pi (TMeasure mu) b -> do
       muv <- whnfMeasure env mu
       bv  <- whnf env b -- not adding measure constraint to context!
@@ -690,6 +696,7 @@
 piApps tv (v:vs) = do tv' <- piApp tv v
                       piApps tv' vs
 
+updateValu :: Valuation -> Int -> Val -> TypeCheck Valuation
 updateValu valu i v = reval' (sgVal i v) valu
 
 -- in app u v, u might be a VDef (e.g. when coming from reval)
@@ -1239,7 +1246,7 @@
     -- Here, we need the type!
     matchVarP x v = do
       let env = fst st
-      case find ((x ==) . fst) $ envMap $ fst st of
+      case List.find ((x ==) . fst) $ envMap $ fst st of
         Nothing     -> return $ Just $ mapFst (\ env -> update env x v) st
         Just (y,v') -> ifM (eqValBool tv v v') (return $ Just st) (return Nothing)
 
@@ -1446,6 +1453,7 @@
   | ShCoSet (OneOrTwo Val)     -- CoSet i and CoSet j
     deriving (Eq, Ord)
 
+shSize :: TypeShape
 shSize = ShSort (ShSortC Size)
 
 -- typeView does not normalize!
@@ -1497,10 +1505,10 @@
     _ -> throwErrorMsg $ "sort " ++ show s1 ++ " has different shape than " ++ show s2
 
 whnf12 :: OneOrTwo Env -> OneOrTwo Expr -> TypeCheck (OneOrTwo Val)
-whnf12 env12 e12 = Traversable.traverse id $ zipWith12 whnf env12 e12
+whnf12 env12 e12 = traverse id $ zipWith12 whnf env12 e12
 
 app12 ::  OneOrTwo Val -> OneOrTwo Val -> TypeCheck (OneOrTwo Val)
-app12 fv12 v12 = Traversable.traverse id $ zipWith12 app fv12 v12
+app12 fv12 v12 = traverse id $ zipWith12 app fv12 v12
 
 -- if m12 = Nothing, we are checking subtyping, otherwise we are
 -- comparing objects or higher-kinded types
@@ -1604,8 +1612,8 @@
                  case mt12 of
                    Nothing -> recoverFail $ "leqVal': cannot compare constructor terms without type"
                    Just tv12 -> do
-                     ct12 <- Traversable.mapM (conType n1) tv12
-                     leqVals' f p ct12 vl1 vl2
+                     ct12 <- mapM (conType n1) tv12
+                     _ <- leqVals' f p ct12 vl1 vl2
                      return ()
 {-
        leqStructural u1 u2 where
@@ -1910,7 +1918,7 @@
 
       (VGen k1, VGen k2) | k1 == k2 -> do
         tv12 <- (fmap typ . domain) <$> lookupGen k1
-        leqVals' f pol tv12 w1 w2
+        _ <- leqVals' f pol tv12 w1 w2
         return ()
 {-
       (VGen k1, VGen k2) ->
@@ -1934,7 +1942,7 @@
 
       (VDef n, VDef m) | n == m ->  do
         tv <- lookupSymbTypQ (idName n)
-        leqVals' f pol (One tv) w1 w2
+        _ <- leqVals' f pol (One tv) w1 w2
         return ()
 
       -- check for least or greatest type
@@ -2290,8 +2298,8 @@
   case pol of
     _ | pol == mixed -> do
       assert (ltle1 == ltle2) $ "unequal bound types"
-      zipWithM (leqSize mixed) mu1  mu2
-      zipWithM (leqSize mixed) mu1' mu2'
+      zipWithM_ (leqSize mixed) mu1  mu2
+      zipWithM_ (leqSize mixed) mu1' mu2'
       return ()
     Pos | ltle1 == Lt || ltle2 == Le  -> do
       lexSizes Le mu2  mu1  -- not strictly smaller
diff --git a/src/Extract.hs b/src/Extract.hs
--- a/src/Extract.hs
+++ b/src/Extract.hs
@@ -150,18 +150,15 @@
 
 import Prelude hiding (pi, null)
 
-import Control.Applicative
-import Control.Monad
-import Control.Monad.Except
-import Control.Monad.Reader
-import Control.Monad.Writer
-import Control.Monad.State
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative ((<$>), (<*>))
+#endif
+import Control.Monad.Except (runExceptT)
+import Control.Monad.Reader (runReaderT)
+import Control.Monad.State  (runStateT)
 
-import Data.Char
-import Data.Traversable (Traversable)
+-- import Data.Char
 import qualified Data.Traversable as Traversable
-import Data.Map (Map)
-import qualified Data.Map as Map
 import qualified Data.Maybe as Maybe
 
 import Text.PrettyPrint
@@ -174,8 +171,10 @@
 import TraceError
 import Util
 
+traceExtrM :: Monad m => String -> m ()
 traceExtrM s = return ()
 
+runExtract :: Signature -> TypeCheck a -> IO (Either TraceError (a, TCState))
 runExtract sig k = runExceptT (runReaderT (runStateT k (initWithSig sig)) emptyContext)
 
 -- extraction
diff --git a/src/HsSyntax.hs b/src/HsSyntax.hs
--- a/src/HsSyntax.hs
+++ b/src/HsSyntax.hs
@@ -1,5 +1,7 @@
 {- 2010-09-17 haskell syntax tools -}
 
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
 module HsSyntax where
 
 import Abstract (PiSigma(..))
diff --git a/src/Lexer.x b/src/Lexer.x
--- a/src/Lexer.x
+++ b/src/Lexer.x
@@ -4,7 +4,7 @@
 {-# OPTIONS_GHC -fno-warn-incomplete-uni-patterns #-}
 {-# OPTIONS_GHC -fno-warn-unused-matches #-}
 
-module Lexer where
+module Lexer (AlexPosn, Token(..), alexScanTokens, prettyTok) where
 
 }
 
diff --git a/src/License.hs b/src/License.hs
new file mode 100644
--- /dev/null
+++ b/src/License.hs
@@ -0,0 +1,35 @@
+-- This file was autogenerated from LICENSE, do not edit!!
+
+{-# LANGUAGE QuasiQuotes #-}
+
+module License where
+
+import Data.String.QQ
+
+copyright :: String
+copyright = head (lines license)
+
+license :: String
+license = [s|
+Copyright (c) 2007-2014 Andreas Abel and Karl Mehltretter.
+
+Permission is hereby granted, free of charge, to any person obtaining
+a copy of this software and associated documentation files (the
+"Software"), to deal in the Software without restriction, including
+without limitation the rights to use, copy, modify, merge, publish,
+distribute, sublicense, and/or sell copies of the Software, and to
+permit persons to whom the Software is furnished to do so, subject to
+the following conditions:
+
+The above copyright notice and this permission notice shall be
+included in all copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY
+CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT,
+TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
+
+|]
diff --git a/src/Main.hs b/src/Main.hs
deleted file mode 100644
--- a/src/Main.hs
+++ /dev/null
@@ -1,137 +0,0 @@
-module Main where
-
-import Prelude hiding (null)
-
-import System.Environment
-import System.Exit
-import System.IO (stdout, hSetBuffering, BufferMode(..))
-
-import qualified Language.Haskell.Exts.Syntax as H
-import qualified Language.Haskell.Exts.Pretty as H
-
-import Lexer
-import Parser
-
-import qualified Concrete as C
-import qualified Abstract as A
-import Abstract (Name)
-import ScopeChecker
-import Value
-import TCM
-import TypeChecker
-import Extract
-import ToHaskell
-
-import Util
-
-main :: IO ()
-main = do
-  hSetBuffering stdout NoBuffering
-  putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"
-  args <- getArgs
-  mapM_ mainFile args
-
-mainFile :: String -> IO ()
-mainFile fileName = do
-  putStrLn $ "--- opening " ++ show fileName ++ " ---"
-  file <- readFile fileName
-  let t = alexScanTokens file
-  let cdecls =  parse t
-  -- putStrLn "--- parsing ---"
-  -- mapM (putStrLn . show) cdecls
-  putStrLn "--- scope checking ---"
-  adecls <- doScopeCheck cdecls
-  -- mapM (putStrLn . show) adecls
-  putStrLn "--- type checking ---"
-  (edecls, sig) <- doTypeCheck adecls
-  putStrLn "--- evaluating ---"
-  showAll sig adecls
-{-
-  putStrLn "--- extracting ---"
-  edecls <- doExtract sig edecls
-  hsmodule <- doTranslate edecls
-  putStrLn $ H.prettyPrint hsmodule
-  -- printHsDecls hsdecls
--}
-  putStrLn $ "--- closing " ++ show fileName ++ " ---"
-
--- print extracted program
-
-ppHsMode :: H.PPHsMode
-ppHsMode = H.PPHsMode  -- H.defaultMode
-  { H.classIndent  = 2
-  , H.doIndent     = 3
-  , H.multiIfIndent = 3
-  , H.caseIndent   = 3
-  , H.letIndent    = 4
-  , H.whereIndent  = 2
-  , H.onsideIndent = 1
-  , H.spacing      = False
-  , H.layout       = H.PPOffsideRule
-  , H.linePragmas  = False
-  }
-
-printHsDecls :: [H.Decl ()] -> IO ()
-printHsDecls hs = mapM_ (putStrLn . H.prettyPrintWithMode ppHsMode) hs
-
--- all let declarations
-allLet :: Signature -> [A.Declaration] -> [(Name,A.Expr)]
-allLet sig [] = []
-allLet sig (decl:xs) =
-    case decl of
-      (A.LetDecl True n tel _ e) | null tel ->
-          (n,e):(allLet sig xs)
-      _ -> allLet sig xs
-
-
-showAll :: Signature -> [A.Declaration] -> IO ()
-showAll sig decl = mapM_ (showLet sig) $ allLet sig decl
-
-showLet :: Signature -> (Name,A.Expr) -> IO ()
-showLet sig (n,e) = do
-  r <- doWhnf sig e
-  case r of
-    Right (v,_) -> putStrLn $ show n ++ " has whnf " ++ show v
-    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
-                      exitFailure
-  r <- doNf sig e
-  case r of
-    Right (v,_) -> putStrLn $ show n ++ " evaluates to " ++ show v
-    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
-                      exitFailure
-
-doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]
-doExtract sig decls = do
-  k <- runExtract sig $ extractDecls decls
-  case k of
-    Left err -> do
-      putStrLn $ "error during extraction:\n" ++ show err
-      exitFailure
-    Right (hs, _) ->
-      return hs
-
-doTranslate :: [A.EDeclaration] -> IO (H.Module ())
-doTranslate decls = do
-  k <- runTranslate $ translateModule decls
-  case k of
-    Left err -> do
-      putStrLn $ "error during extraction:\n" ++ show err
-      exitFailure
-    Right hs ->
-      return hs
-
-doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)
-doTypeCheck decls = do
-  k <- typeCheck decls
-  case k of
-    Left err -> do
-      putStrLn $ "error during typechecking:\n" ++ show err
-      exitFailure
-    Right (edecls, st) ->
-      return (edecls, signature st)
-
-doScopeCheck :: [C.Declaration] -> IO [A.Declaration]
-doScopeCheck decl = case scopeCheck decl of
-     Left err -> do putStrLn $ "scope check error: " ++ show err
-                    exitFailure
-     Right (decl',_) -> return $ decl'
diff --git a/src/MainLib.hs b/src/MainLib.hs
new file mode 100644
--- /dev/null
+++ b/src/MainLib.hs
@@ -0,0 +1,138 @@
+module MainLib where
+
+import Prelude hiding (null, mapM_)
+
+import Data.Foldable (mapM_)
+
+import System.Exit
+import System.IO (stdout, hSetBuffering, BufferMode(..))
+
+import qualified Language.Haskell.Exts.Syntax as H
+import qualified Language.Haskell.Exts.Pretty as H
+
+import Lexer
+import Parser
+import Options
+
+import qualified Concrete as C
+import qualified Abstract as A
+import Abstract (Name)
+import ScopeChecker
+import TCM
+import TypeChecker
+import Extract
+import ToHaskell
+
+import Util
+
+main :: IO ()
+main = do
+  hSetBuffering stdout NoBuffering
+  -- putStrLn "MiniAgda by Andreas Abel and Karl Mehltretter"
+  opts <- options
+  mapM_ mainFile $ optInputs opts
+
+mainFile :: String -> IO ()
+mainFile fileName = do
+  putStrLn $ "--- opening " ++ show fileName ++ " ---"
+  file <- readFile fileName
+  let t = alexScanTokens file
+  let cdecls =  parse t
+  -- putStrLn "--- parsing ---"
+  -- mapM (putStrLn . show) cdecls
+  putStrLn "--- scope checking ---"
+  adecls <- doScopeCheck cdecls
+  -- mapM (putStrLn . show) adecls
+  putStrLn "--- type checking ---"
+  (edecls, sig) <- doTypeCheck adecls
+  putStrLn "--- evaluating ---"
+  showAll sig adecls
+{-
+  putStrLn "--- extracting ---"
+  edecls <- doExtract sig edecls
+  hsmodule <- doTranslate edecls
+  putStrLn $ H.prettyPrint hsmodule
+  -- printHsDecls hsdecls
+-}
+  putStrLn $ "--- closing " ++ show fileName ++ " ---"
+
+-- print extracted program
+
+ppHsMode :: H.PPHsMode
+ppHsMode = H.PPHsMode  -- H.defaultMode
+  { H.classIndent  = 2
+  , H.doIndent     = 3
+  , H.multiIfIndent = 3
+  , H.caseIndent   = 3
+  , H.letIndent    = 4
+  , H.whereIndent  = 2
+  , H.onsideIndent = 1
+  , H.spacing      = False
+  , H.layout       = H.PPOffsideRule
+  , H.linePragmas  = False
+  }
+
+printHsDecls :: [H.Decl ()] -> IO ()
+printHsDecls hs = mapM_ (putStrLn . H.prettyPrintWithMode ppHsMode) hs
+
+-- all let declarations
+allLet :: Signature -> [A.Declaration] -> [(Name,A.Expr)]
+allLet sig [] = []
+allLet sig (decl:xs) =
+    case decl of
+      (A.LetDecl True n tel _ e) | null tel ->
+          (n,e):(allLet sig xs)
+      _ -> allLet sig xs
+
+
+showAll :: Signature -> [A.Declaration] -> IO ()
+showAll sig decl = mapM_ (showLet sig) $ allLet sig decl
+
+showLet :: Signature -> (Name,A.Expr) -> IO ()
+showLet sig (n,e) = do
+  r <- doWhnf sig e
+  case r of
+    Right (v,_) -> putStrLn $ show n ++ " has whnf " ++ show v
+    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
+                      exitFailure
+  r <- doNf sig e
+  case r of
+    Right (v,_) -> putStrLn $ show n ++ " evaluates to " ++ show v
+    Left err    -> do putStrLn $ "error during evaluation:\n" ++ show err
+                      exitFailure
+
+doExtract :: Signature -> [A.EDeclaration] -> IO [A.EDeclaration]
+doExtract sig decls = do
+  k <- runExtract sig $ extractDecls decls
+  case k of
+    Left err -> do
+      putStrLn $ "error during extraction:\n" ++ show err
+      exitFailure
+    Right (hs, _) ->
+      return hs
+
+doTranslate :: [A.EDeclaration] -> IO (H.Module ())
+doTranslate decls = do
+  k <- runTranslate $ translateModule decls
+  case k of
+    Left err -> do
+      putStrLn $ "error during extraction:\n" ++ show err
+      exitFailure
+    Right hs ->
+      return hs
+
+doTypeCheck :: [A.Declaration] -> IO ([A.EDeclaration], Signature)
+doTypeCheck decls = do
+  k <- typeCheck decls
+  case k of
+    Left err -> do
+      putStrLn $ "error during typechecking:\n" ++ show err
+      exitFailure
+    Right (edecls, st) ->
+      return (edecls, signature st)
+
+doScopeCheck :: [C.Declaration] -> IO [A.Declaration]
+doScopeCheck decl = case scopeCheck decl of
+     Left err -> do putStrLn $ "scope check error: " ++ show err
+                    exitFailure
+     Right (decl',_) -> return $ decl'
diff --git a/src/Makefile b/src/Makefile
--- a/src/Makefile
+++ b/src/Makefile
@@ -17,6 +17,37 @@
 default : Main test
 all : Main test examples lib
 
+# Generate License.hs
+#####################
+
+.PHONY: license
+
+license: License.hs
+
+License.hs : ../LICENSE Makefile
+	echo "\
+-- This file was autogenerated from LICENSE, do not edit!!\n\n\
+{-# LANGUAGE QuasiQuotes #-}\n\n\
+module License where\n\n\
+import Data.String.QQ\n\n\
+copyright :: String\n\
+copyright = head (lines license)\n\n\
+license :: String\n\
+license = [s|" > $@
+	cat $< >> $@
+	echo "\n|]" >> $@
+
+# Generate emacs tags
+#####################
+
+.PHONY: TAGS
+
+TAGS :
+	hasktags -e *.hs
+
+# Building
+##########
+
 prof-current : miniagda-prof
 	miniagda-prof ../examples/FiCS12/fics12-06.ma +RTS -prof -s
 #	miniagda-prof ../test/succeed/Zero.ma +RTS -prof -s
@@ -74,6 +105,9 @@
 %arser.hs : %arser.y Lexer.hs
 	happy --info=$<-grm.txt $<
 
+# Testing
+#########
+
 test : Main succeed fail
 
 succeed :
@@ -100,6 +134,8 @@
 	@echo "======================================================================"
 	make -C ../lib
 
+# Cleaning
+##########
 
 clean :
 	-rm *.o *.hi Main miniagda-prof
diff --git a/src/Options.hs b/src/Options.hs
new file mode 100644
--- /dev/null
+++ b/src/Options.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE CPP #-}
+
+-- | Options given to @MiniAgda@.
+
+module Options where
+
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup               ( (<>) )
+#endif
+
+import Options.Applicative
+import Options.Applicative.NonEmpty ( some1 )
+
+import System.Environment           ( getArgs )
+
+import License                      ( copyright, license )
+import Util
+import Version                      ( version )
+
+-- | Options given to @MiniAgda@.
+data Options = Options
+  { optInputs :: List1 FilePath
+      -- ^ The source files to type check, from first to last.
+  }
+
+self :: String
+self = "MiniAgda"
+
+-- | Parse the options given on the command line.
+options :: IO Options
+options = handleParseResult =<< do parseOptions <$> getArgs
+
+-- | Pure parser for command line given by a list of strings.
+parseOptions :: [String] -> ParserResult Options
+parseOptions = execParserPure defaultPrefs $ info parser description
+  where
+  parser = theOptions <**>
+    (versionOption <*> numericVersionOption <*> licenseOption <*> helper)
+
+  description = header top <> footer bot
+  top = unwords
+    [ concat [ self, ":" ]
+    , "A prototypical dependently typed pure language with sized types."
+    ]
+  bot = unwords
+    [ "Checks the given MiniAgda files in first-to-last order."
+    , "Later files can refer to definitions made in earlier files."
+    ]
+
+  versionOption =
+    infoOption versionLong
+      $  long "version"
+      <> short 'V'
+      <> help "Show version info."
+      <> hidden
+  versionText = unwords [ self, "version", version ]
+  versionLong = intercalate "\n" $
+    [ versionText
+    , copyright
+    , "This is free software under the MIT license."
+    ]
+
+  numericVersionOption =
+    infoOption version
+      $  long "numeric-version"
+      <> help "Show just version number."
+      <> hidden
+
+  licenseOption =
+    infoOption license
+      $  long "license"
+      <> help "Show the license text."
+      <> hidden
+
+  theOptions = Options
+    <$> oInputs
+
+  oInputs :: Parser (List1 FilePath)
+  oInputs = some1 $
+    strArgument
+      $  metavar "FILES"
+      <> action "file"
+      <> help "Files to check (in first-to-last order)."
diff --git a/src/Parser.y b/src/Parser.y
--- a/src/Parser.y
+++ b/src/Parser.y
@@ -1,6 +1,6 @@
 {
 {-# LANGUAGE BangPatterns #-}
-module Parser where
+module Parser (parse) where
 
 import qualified Lexer as T
 import qualified Concrete as C
diff --git a/src/PrettyTCM.hs b/src/PrettyTCM.hs
--- a/src/PrettyTCM.hs
+++ b/src/PrettyTCM.hs
@@ -1,6 +1,8 @@
 {-# LANGUAGE TypeSynonymInstances, FlexibleInstances #-}
 {-# LANGUAGE NoImplicitPrelude #-}
 
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
 module PrettyTCM where
 
 import Prelude hiding (sequence, mapM, (<>))
@@ -11,7 +13,9 @@
 import qualified Util
 import Value
 
-import Control.Applicative hiding (empty)
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative ((<$>), (<*>))
+#endif
 import Control.Monad ((<=<))
 import Data.Traversable
 
diff --git a/src/ScopeChecker.hs b/src/ScopeChecker.hs
--- a/src/ScopeChecker.hs
+++ b/src/ScopeChecker.hs
@@ -5,11 +5,15 @@
       FlexibleContexts, FlexibleInstances, UndecidableInstances,
       MultiParamTypeClasses #-}
 
+{-# OPTIONS_GHC -fno-warn-missing-signatures #-}
+
 module ScopeChecker (scopeCheck) where
 
 import Prelude hiding (mapM, null)
 
+#if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
+#endif
 import Control.Monad          hiding (mapM)
 import Control.Monad.Identity (Identity, runIdentity)
 import Control.Monad.Reader   (ReaderT, runReaderT, MonadReader, ask, asks, local)
@@ -22,11 +26,14 @@
 import Data.Maybe
 import Data.Traversable (mapM)
 
-import Debug.Trace
+-- import Debug.Trace
 
 import Polarity(Pol(..))
 import qualified Polarity as A
-import Abstract (Sized,mkExtRef,Co,ConK(..),PrePost(..),MVar,Decoration(..),Override(..),Measure(..),adjustTopDecsM,Arity,polarity,LensPol(..))
+import Abstract
+  ( Sized, Co, ConK(..), PrePost(..), MVar, Override(..), Measure(..), adjustTopDecsM
+  , Arity, polarity, LensPol(..)
+  )
 import qualified Abstract as A
 import qualified Concrete as C
 
@@ -34,13 +41,13 @@
 
 import Util
 
--- * scope checker
--- check that all identifiers are in scope and global identifiers are only used once
--- replaces Ident with Con, Def, Let or Var
--- replaces IdentP with ConP or VarP in patterns
--- replaces Unknown by a new Meta-Variable
--- check pattern length is equal in each clause
--- group mutual declarations
+-- * Scope checker.
+-- - check that all identifiers are in scope and global identifiers are only used once
+-- - replaces Ident with Con, Def, Let or Var
+-- - replaces IdentP with ConP or VarP in patterns
+-- - replaces Unknown by a new Meta-Variable
+-- - check pattern length is equal in each clause
+-- - group mutual declarations
 
 -- | Entry point for scope checker.
 scopeCheck :: [C.Declaration] -> Either TraceError ([A.Declaration],SCState)
@@ -145,6 +152,7 @@
   , nextPolVar :: MVar
   }
 
+initSt :: SCState
 initSt = SCState emptySig 0 0
 
 -- * The scope checking monad.
@@ -539,7 +547,7 @@
 addFields :: IKind -> Context -> [C.Name] -> ScopeCheck [A.Name]
 addFields kind delta cfields = do
     afields <- mapM (scopeCheckField delta) cfields
-    mapM (uncurry $ addANameU kind) $ zip cfields afields
+    mapM_ (uncurry $ addANameU kind) $ zip cfields afields
     return afields
 
 scopeCheckDataDecl :: C.Declaration -> ScopeCheck A.Declaration
@@ -608,12 +616,12 @@
   --let addFuns b = mapM (uncurry $ addAName $ FunK b) nxs
 --  let addFuns b = mapM (\ (n,x) -> addAName (FunK b) n x) nxs
   -- addFuns False
-  mapM (uncurry $ addANameU $ FunK False) nxs
+  mapM_ (uncurry $ addANameU $ FunK False) nxs
   arcll' <- mapM (setDefaultPolarity A.Rec . scopeCheckFunClauses) l
   -- add names as external ids
   --addFuns True
   let nxs' = map (mapPair id A.mkExtName) nxs
-  mapM (uncurry $ addANameU (LetK)) nxs'
+  mapM_ (uncurry $ addANameU (LetK)) nxs'
 --  mapM (uncurry $ addAName (FunK True)) nxs'
   return $ A.MutualFunDecl (isJust ml) co $
     zipWith3 (\ ts (_, x') (ar, cls) -> A.Fun ts x' ar cls) tsl' nxs' arcll'
diff --git a/src/TCM.hs b/src/TCM.hs
--- a/src/TCM.hs
+++ b/src/TCM.hs
@@ -9,18 +9,18 @@
 import Control.Monad.Except (ExceptT, MonadError)
 import Control.Monad.Reader (ReaderT, ask, asks, local)
 
+#if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
 import Data.Foldable (Foldable)
-import qualified Data.Foldable as Foldable
 import Data.Traversable (Traversable)
+#endif
 import qualified Data.Traversable as Traversable
-import Data.Monoid
 
 import Data.Map (Map)
 import qualified Data.Map as Map
 import qualified Data.Maybe as Maybe
 
-import Debug.Trace
+-- import Debug.Trace
 
 import Abstract
 import Polarity
@@ -38,10 +38,14 @@
 
 import Warshall
 
+traceSig :: String -> a -> a
 -- traceSig msg a = trace msg a
 traceSig msg a = a
 
+traceRew :: String -> a -> a
 traceRew msg a = a -- trace msg a
+
+traceRewM :: Monad m => String -> m ()
 traceRewM msg = return () -- traceM msg
 {-
 traceRew msg a = trace msg a
@@ -50,7 +54,10 @@
 
 -- metavariables and constraints
 
+traceMeta :: String -> a -> a
 traceMeta msg a = a -- trace msg a
+
+traceMetaM :: Monad m => String -> m ()
 traceMetaM msg = return () -- traceM msg
 {-
 traceMeta msg a = trace msg a
@@ -179,6 +186,7 @@
 instance Show TCContext where
     show ce = show (environ ce) ++ "; " ++ show (context ce)
 
+emptyContext :: TCContext
 emptyContext = TCContext
   { context  = cxtEmpty
   , renaming = Map.empty
@@ -211,6 +219,8 @@
   }
 
 type MetaVars = Map MVar MetaVar
+
+emptyMetaVars :: MetaVars
 emptyMetaVars = Map.empty
 
 type MScope = [Name] -- ^ names of size variables which are in scope of mvar
@@ -221,6 +231,8 @@
 
 type PosConstrnt = Constrnt PPoly DefId ()
 type PositivityGraph = [PosConstrnt]
+
+emptyPosGraph :: PositivityGraph
 emptyPosGraph = []
 
 -- type TypeCheck = StateT TCState (ReaderT TCContext (CallStackT String IO))
@@ -276,6 +288,7 @@
 data Rewrite  = Rewrite { lhs :: Val,  rhs :: Val }
 type Rewrites = [Rewrite]
 
+emptyRewrites :: Rewrites
 emptyRewrites = []
 
 instance Show Rewrite where
@@ -349,6 +362,8 @@
       (Map.elems (decs delta))
     ) (Map.elems (upperDecs delta))
 -}
+
+cxtEmpty :: SemCxt
 cxtEmpty = SemCxt
   { len = 0
   , cxt = Map.empty
@@ -431,15 +446,6 @@
 cxtApplyDec dec delta = delta { upperDecs = Map.map (compDec dec) (upperDecs delta) }
 -- cxtApplyDec dec delta =  delta { decs = Map.map (fmap $ invCompDec dec) (decs delta) }
 
-{- RETIRED, use cxtApplyDec instead
--- clear all "erased" flags (see Pfenning, LICS 2001)
--- UPDATE: resurrection sets "target" status to erased
---         (as opposed to setting "source" status to non-erased)
-cxtResurrect :: SemCxt -> SemCxt
-cxtResurrect delta = delta { upperDecs = Map.map (\ dec -> dec { erased = True}) (upperDecs delta) }
--- cxtResurrect delta = delta { decs = Map.map (fmap resurrectDec) (decs delta) }
--}
-
 -- manipulating the context ------------------------------------------
 
 {-
@@ -533,6 +539,7 @@
   goImpredicative :: m a -> m a
   checkingMutual :: Maybe DefId -> m a -> m a
 
+dontCare :: a
 dontCare = error "Internal error: tried to retrieve unassigned type of variable"
 
 instance MonadCxt TypeCheck where
@@ -898,6 +905,7 @@
 underAbs_  :: Name -> Domain -> FVal -> (Int -> Val -> Val -> TypeCheck a) -> TypeCheck a
 underAbs_ x dom fv cont = noConsistencyChecking $ underAbs x dom fv cont
 
+noConsistencyChecking :: TypeCheck a -> TypeCheck a
 noConsistencyChecking = local $ \ cxt -> cxt { consistencyCheck = False }
 
 -- | No eta, no hypotheses.  First returned val is a @VGen i@.
@@ -1006,10 +1014,10 @@
 type Signature = Map QName SigDef
 
 -- a signature entry is either
--- * a fun/cofun,
--- * a defined constant,
--- * a constructor, or
--- * a data type id with its kind
+-- - a fun/cofun,
+-- - a defined constant,
+-- - a constructor, or
+-- - a data type id with its kind
 -- they share "symbTyp", the type signature of the definition
 data SigDef
   = FunSig  { isCo          :: Co
@@ -1104,6 +1112,7 @@
 symbKind DataSig{} = kType          -- data types are never universes
 -}
 
+emptySig :: Signature
 emptySig = Map.empty
 
 -- Handling constructor types  ------------------------------------------
@@ -1383,12 +1392,12 @@
     if any id bs then return Nothing else
      throwErrorMsg $ "cannot handle constraint " ++ show v ++ " <= " ++ show (VMax vs)
   mkConstraint w@(VMax vs) v = throwErrorMsg $ "cannot handle constraint " ++ show w ++ " <= " ++ show v
-  mkConstraint (VMeta i rho n) (VMeta j rho' m) = retret $ arc (Flex i) (m-n) (Flex j)
-  mkConstraint (VMeta i rho n) VInfty      = retret $ arc (Flex i) 0 (Rigid (RConst Infinite))
-  mkConstraint (VMeta i rho n) v           = retret $ arc (Flex i) (m-n) (Rigid (RVar j))
+  mkConstraint (VMeta i rho n) (VMeta j rho' m) = return $ Just $ arc (Flex i) (m-n) (Flex j)
+  mkConstraint (VMeta i rho n) VInfty      = return $ Just $ arc (Flex i) 0 (Rigid (RConst Infinite))
+  mkConstraint (VMeta i rho n) v           = return $ Just $ arc (Flex i) (m-n) (Rigid (RVar j))
     where (j,m) = vGenSuccs v 0
-  mkConstraint VInfty (VMeta i rho n)      = retret $ arc (Rigid (RConst Infinite)) 0 (Flex i)
-  mkConstraint v (VMeta j rho m)           = retret $ arc (Rigid (RVar i)) (m-n) (Flex j)
+  mkConstraint VInfty (VMeta i rho n)      = return $ Just $ arc (Rigid (RConst Infinite)) 0 (Flex i)
+  mkConstraint v (VMeta j rho m)           = return $ Just $ arc (Rigid (RVar i)) (m-n) (Flex j)
     where (i,n) = vGenSuccs v 0
   mkConstraint v1 v2 = throwErrorMsg $ "mkConstraint undefined for " ++ show (v1,v2)
 
@@ -1428,11 +1437,10 @@
 nameOf ((x,VGen i):rho) j | i == j = Just x
 nameOf (_:rho) j = nameOf rho j
 
+vGenSuccs :: Val -> Int -> (Int, Int)
 vGenSuccs (VGen k)  m = (k,m)
 vGenSuccs (VSucc v) m = vGenSuccs v (m+1)
 vGenSuccs v m = error $ "vGenSuccs fails on " ++ Util.parens (show v) ++ " " ++ show m
-
-retret = return . return
 
 sizeExprToExpr :: Env -> SizeExpr -> Expr
 sizeExprToExpr rho (SizeConst Infinite) = Infty
diff --git a/src/Termination.hs b/src/Termination.hs
--- a/src/Termination.hs
+++ b/src/Termination.hs
@@ -9,11 +9,9 @@
 
 import qualified Data.List as List
 import Data.Monoid
-import Data.Set (Set)
-import qualified Data.Set as Set
-import Data.Foldable (Foldable, foldMap)
-import qualified Data.Foldable as Foldable
-
+#if !MIN_VERSION_base(4,8,0)
+import Data.Foldable (foldMap)
+#endif
 import Debug.Trace
 
 --import System
@@ -28,7 +26,10 @@
 import TreeShapedOrder (TSO)
 import qualified TreeShapedOrder as TSO
 
+traceTerm :: String -> a -> a
 traceTerm msg a = a -- trace msg a
+
+traceTermM :: Monad m => String -> m ()
 traceTermM msg = return () -- traceM msg
 {-
 traceTerm msg a = trace msg a
@@ -36,7 +37,10 @@
 -}
 
 
+traceProg :: String -> a -> a
 traceProg msg a =  a
+
+traceProgM :: Monad m => String -> m ()
 traceProgM msg = return ()
 {-
 traceProg msg a = trace msg a
@@ -336,6 +340,7 @@
       ((Proj Post n1,[]), ProjP n2) | n1 == n2 -> Decr 0
       _ -> Un
 
+conView :: (Expr, [Expr]) -> (Expr, [Expr])
 conView (Record (NamedRec co n _ _) rs, es) = (Def (DefId (ConK co) n), map snd rs ++ es)
 conView p = p
 
@@ -495,11 +500,11 @@
 type Progress = Writer Any
 type ProgressH = Writer (Any, Any)
 
+firstHalf :: (Any, Any)
 firstHalf = (Any True, Any False)
-secondHalf = (Any False, Any True)
 
--- fullProgress = Sum 2
--- halfProgress = Sum 1
+secondHalf :: (Any, Any)
+secondHalf = (Any False, Any True)
 
 -- we keep CMSets always in normal form
 -- progress reported if m is "better" than one of ms
@@ -711,11 +716,6 @@
 groupCalls (n:nl) cl = (n, [ c | c <- cl , (source c == n) ]) : groupCalls nl cl
 -}
 
-{-
-ccFunDecl :: [ ( TypeSig,[Clause]) ] -> [Call]
-ccFunDecl funs = complete $ collectCGFunDecl funs
--}
-
 collectCGFunDecl :: (?cutoff :: Int) => [(Name,Arity)] -> [Fun] -> [Call]
 collectCGFunDecl names funs =
       concatMap (collectClauses names) funs
@@ -729,18 +729,6 @@
                 (collectCallsExpr names n pl rhs) ++ (collectClause names n rest)
             collectClause names n [] = []
 
-{- RETIRED
-arity :: [Clause] -> Int
-arity [] = 0
-arity (Clause pl e:l) = length pl
--}
-
-{- RETIRED (map)
-collectNames :: [Fun] -> [(Name,Arity)]
-collectNames [] = []
-collectNames (Fun (TypeSig n _) ar cls : rest) = (n,ar) : (collectNames rest)
--}
-
 -- | harvest i > j  from  case i { $ j -> ...}
 tsoCase :: TSO Name -> Expr -> [Clause] -> TSO Name
 tsoCase tso (Var x) [Clause _ [SuccP (VarP y)] _] = TSO.insert y (1,x) tso
@@ -783,8 +771,8 @@
              (loop tso e1) ++ -- type won't get evaluated
              (loop tso e2)
           (Quant _ tb@(TBind x dom) e2) -> (loop tso (typ dom)) ++ (loop (tsoBind tso tb) e2)
-          (Quant _ (TMeasure mu) e2) -> Foldable.foldMap (loop tso) mu ++ (loop tso e2)
-          (Quant _ (TBound beta) e2) -> Foldable.foldMap (loop tso) beta ++ (loop tso e2)
+          (Quant _ (TMeasure mu) e2) -> foldMap (loop tso) mu ++ (loop tso e2)
+          (Quant _ (TBound beta) e2) -> foldMap (loop tso) beta ++ (loop tso e2)
           (Below ltle e) -> loop tso e
           (Sing e1 e2) -> (loop tso e1) ++ (loop tso e2)
           (Pair e1 e2) -> (loop tso e1) ++ (loop tso e2)
@@ -800,7 +788,7 @@
           Def{}   -> []
           Irr{}   -> []
           Proj{}   -> []
-          Record ri rs -> Foldable.foldMap (loop tso . snd) rs
+          Record ri rs -> foldMap (loop tso . snd) rs
           Ann e1 -> loop tso (unTag e1)
 --          Con{}   -> []
 --          Let{}   -> []
diff --git a/src/ToHaskell.hs b/src/ToHaskell.hs
--- a/src/ToHaskell.hs
+++ b/src/ToHaskell.hs
@@ -43,19 +43,17 @@
 
 import Data.Char
 
-import Control.Applicative
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative ((<$>), (<*>))
+#endif
 import Control.Monad
-import Control.Monad.Except
-import Control.Monad.Reader
-import Control.Monad.Writer
-import Control.Monad.State
+import Control.Monad.Except (ExceptT, runExceptT)
+import Control.Monad.Reader (ReaderT, runReaderT)
+import Control.Monad.State  (StateT, evalStateT)
 
-import Data.Map (Map)
-import qualified Data.Map as Map
 import qualified Data.Traversable as Trav
 
 import qualified Language.Haskell.Exts.Syntax as Hs
-import Text.PrettyPrint
 
 import Polarity
 import Abstract
diff --git a/src/Tokens.hs b/src/Tokens.hs
deleted file mode 100644
--- a/src/Tokens.hs
+++ /dev/null
@@ -1,28 +0,0 @@
-module Tokens where
-
-data Token
-  = Id String
-  | Data
-  | Fun
-  | Def
-  | Mutual
-  | Pattern
-  | Set
-  | Case
-  -- size type
-  | Size
-  | Infty
-  | Succ
-  --
-  | BrOpen
-  | BrClose
-  | PrOpen
-  | PrClose
-  | Sem
-  | Col
-  | Arrow
-  | Eq
-  | Lam
-  | UScore
-  | NotUsed -- so happy doesn't generate overlap case pattern warning
-    deriving (Eq,Ord,Show)
diff --git a/src/TraceError.hs b/src/TraceError.hs
--- a/src/TraceError.hs
+++ b/src/TraceError.hs
@@ -1,8 +1,9 @@
+{-# LANGUAGE CPP #-}
 {-# LANGUAGE MultiParamTypeClasses, FlexibleContexts #-}
 
 module TraceError where
 
-import Control.Monad.Except
+import Control.Monad.Except   (MonadError, throwError, catchError)
 import Control.Monad.IO.Class (MonadIO(..))
 import Debug.Trace
 
@@ -63,10 +64,12 @@
 boolToError msg False = throwErrorMsg msg
 
 -- defined in Control.Monad.Error.Class in mtl-2.2.2
--- instance MonadError () Maybe where
---   catchError Nothing k = k ()
---   catchError (Just a) k = Just a
---   throwError () = Nothing
+#if !MIN_VERSION_mtl(2,2,2)
+instance MonadError () Maybe where
+  catchError Nothing k = k ()
+  catchError (Just a) k = Just a
+  throwError () = Nothing
+#endif
 
 orM :: (MonadError e m) => m a -> m a -> m a
 orM m1 m2 = m1 `catchError` (const m2)
diff --git a/src/TypeChecker.hs b/src/TypeChecker.hs
--- a/src/TypeChecker.hs
+++ b/src/TypeChecker.hs
@@ -5,27 +5,26 @@
 
 import Prelude hiding (null)
 
-import Control.Applicative hiding (Const) -- ((<$>))
-import Control.Monad
+#if !MIN_VERSION_base(4,8,0)
+import Control.Applicative ((<$>), (<*>))
+#endif
+import Control.Monad          (foldM, forM, forM_, liftM, unless, when, zipWithM, zipWithM_)
 import Control.Monad.IO.Class (MonadIO(..))
 import Control.Monad.State    (runStateT, get, gets, put)
 import Control.Monad.Except   (runExceptT, catchError)
 import Control.Monad.Reader   (runReaderT, ask, asks, local)
-import Control.Monad.Trans    (lift)
 
 import qualified Data.List as List
 import Data.Map (Map)
-import qualified Data.Map as Map
 import Data.Maybe
 import qualified Data.Foldable as Foldable
 import qualified Data.Traversable as Traversable
 
-import Debug.Trace (trace)
+-- import Debug.Trace (trace)
 
 import qualified Text.PrettyPrint as PP
 
 import Util
-import qualified Util as Util
 
 import Abstract hiding (Substitute)
 import Polarity as Pol
@@ -33,18 +32,18 @@
 import TCM
 import Eval
 import Extract
--- import SPos (nocc) -- RETIRED
 -- import CallStack
 import PrettyTCM
 import TraceError
 
-import Warshall hiding (Flex) -- size constraint checking
-
 import Termination
 
 -- import Completness
 
+traceCheck, traceSing, traceAdm :: String -> a -> a
+traceCheckM, traceSingM, traceAdmM :: Monad m => String -> m ()
 
+
 traceCheck msg a = a -- trace msg a
 traceCheckM msg = return () -- traceM msg
 {-
@@ -71,16 +70,20 @@
 runWhnf sig tc = (runExceptT (runStateT tc  sig))
 -}
 
+doNf :: Signature -> Expr -> IO (Either TraceError (Expr, TCState))
 doNf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= reify) (initWithSig sig)) emptyContext)
+
+doWhnf :: Signature -> Expr -> IO (Either TraceError (Val, TCState))
 doWhnf sig e = runExceptT (runReaderT (runStateT (whnf emptyEnv e >>= whnfClos) (initWithSig sig)) emptyContext)
 
 
 -- top-level functions -------------------------------------------
 
-runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a,TCState))
+runTypeCheck :: TCState -> TypeCheck a -> IO (Either TraceError (a, TCState))
 runTypeCheck st tc = runExceptT (runReaderT (runStateT tc st) emptyContext)
 -- runTypeCheck st tc = runCallStackT (runReaderT (runStateT tc st) emptyContext) []
 
+typeCheck :: [Declaration] -> IO (Either TraceError ([EDeclaration], TCState))
 typeCheck dl = runTypeCheck initSt (typeCheckDecls dl)
 
 -- checking top-level declarations -------------------------------
@@ -88,6 +91,7 @@
 echo :: MonadIO m => String -> m ()
 echo = liftIO . putStrLn
 
+echoR :: MonadIO m => String -> m ()
 echoR = echo
 -- echoR s = echo $ "R> " ++ s
 
@@ -100,6 +104,7 @@
 echoKindedDef :: (Show n, MonadIO m) => Kind -> n -> Expr -> m ()
 echoKindedDef ki n t = echo $ prettyKind ki ++ "  " ++ show n ++ " = " ++ show t
 
+echoEPrefix :: String
 echoEPrefix = "E> "
 
 echoTySigE :: (Show n, MonadIO m) => n -> Expr -> m ()
@@ -122,7 +127,7 @@
 typeCheckDeclaration :: Declaration -> TypeCheck [EDeclaration]
 typeCheckDeclaration (OverrideDecl Check ds) = do
   st <- get
-  typeCheckDecls ds
+  _ <- typeCheckDecls ds
   put st             -- forget the effect of these decls
   return []
 typeCheckDeclaration (OverrideDecl Fail ds) = do
@@ -550,7 +555,7 @@
         echoR $ (PP.render $ prettyFun n cls))
       funse
     -- replace in signature by erased clauses
-    zipWithM (enableSig co) (zipWith intersectKind kis $ map kindOf kfse) funse
+    zipWithM_ (enableSig co) (zipWith intersectKind kis $ map kindOf kfse) funse
     return $ funse
 
   where
@@ -593,7 +598,7 @@
     kfse <- mapM typeCheckFunSig funs0
     let kfuns = zipWith (\ (Kinded ki ts) (Fun ts0 n' ar cls) -> Kinded ki (Fun ts n' ar cls)) kfse funs0
     -- zipWithM (addFunSig co) (map kindOf kfse) funs
-    mapM (addFunSig co) kfuns
+    mapM_ (addFunSig co) kfuns
     let funs = map valueOf kfuns
     -- type check and solve size constraints
     -- return clauses with meta vars resolved
@@ -619,7 +624,7 @@
       funse
     terminationCheck funse
     -- replace in signature by erased clauses
-    zipWithM enableSig kis funse
+    zipWithM_ enableSig kis funse
     return $ funse
 
 addFunSig :: Co -> Kinded Fun -> TypeCheck ()
@@ -708,26 +713,11 @@
   case tv of
     VApp (VDef (DefId DatK (QName n))) vs | n == d -> do
       telvs <- mapM (\ tb -> whnf' (Var (boundName tb))) $ telescope tel
-      enter ("checking datatype parameters in constructor target") $
+      _ <- enter ("checking datatype parameters in constructor target") $
         leqVals' N mixed (One dv) (take (size tel) vs) telvs
       return ()
     _ -> throwErrorMsg $ "constructor should produce something in data type " ++ show d
 
-{- RETIRED (syntactic check)
-checkTarget :: Name -> Telescope -> Type -> TypeCheck ()
-checkTarget d tel tg =
-    case spineView tg of
-      (Def (DefId Dat n), args) | n == d -> checkParams tel (take (length tel) args)
-      _ -> throwErrorMsg $ "target mismatch"  ++ show tg
-
-    where checkParams :: Telescope -> [Expr] -> TypeCheck ()
-          checkParams [] [] = return ()
-          checkParams (tb : tl) ((Var n') : el) | boundName tb == n'
-            = checkParams tl el
-          checkParams tl al = throwErrorMsg $ "target param mismatch " ++
-            d ++ " " ++ show tel ++ " != " ++ show tg ++ "\ncheckParams " ++ show tl ++ " " ++ show al ++ " failed"
--}
-
 -- check that params are types
 -- check that arguments are stypes
 -- check that target is set
@@ -1212,6 +1202,7 @@
   (knes, tv) <- checkSpine es tv
   return (kne : knes, tv)
 
+maybeErase :: Polarity pol => pol -> Expr -> Expr
 maybeErase dec = if erased dec then erasedExpr else id
 
 -- | checking e against (x : A) -> B returns (x,e) and B[e/x]
@@ -1623,7 +1614,7 @@
       -- clearDots -- NOT NEEDED
       (flex,ins,cxt,vt,pe,pv,absp) <- checkPattern neutral [] emptySub tv p
       local (\ _ -> cxt) $ do
-        mapM (checkGoal ins) flex
+        mapM_ (checkGoal ins) flex
         tel <- getContextTele -- TODO!
         case (absp,mrhs) of
            (True,Nothing) -> return $ Kinded NoKind (Clause tel [pe] Nothing)
@@ -1673,7 +1664,7 @@
     -- Note that cofuns need not be SN, so the strict consistency may be
     -- not necessary.
     local (\ _ -> cxt { consistencyCheck = (mutualCo cxt == Ind) }) $ do
-      mapM (checkGoal ins) flex
+      mapM_ (checkGoal ins) flex
 {-
       dots <- openDots
       unless (null dots) $
@@ -1696,8 +1687,13 @@
 
 type Substitution = Valuation -- [(Int,Val)]
 
-emptySub    = emptyVal
-sgSub       = sgVal
+emptySub :: Substitution
+emptySub = emptyVal
+
+sgSub :: Int -> Val -> Substitution
+sgSub = sgVal
+
+lookupSub :: Int -> Substitution -> Maybe Val
 lookupSub i = lookup i . valuation
 
 type DotFlex = (Int,(Expr,Domain))
@@ -2152,23 +2148,7 @@
   check  List ($ j) <= List i
  -}
 
-{- RETIRED
 -- checkDot does not need to extract
-checkDot :: Substitution -> DotFlex -> TypeCheck ()
-checkDot subst (i,(e,it)) = enter ("dot pattern " ++ show e) $
-  case (lookup i subst) of
-    Nothing -> throwErrorMsg $ "not instantiated"
-    Just v -> do
-      tv <- substitute subst (typ it)
-      ask >>= \ ce -> traceCheckM ("checking dot pattern " ++ show ce ++ " |- " ++ show e ++ " : " ++ show (decor it) ++ " " ++ show tv)
-      applyDec (decor it) $ do
-        checkExpr e tv
-        v' <-  whnf' e -- TODO: has subst erased terms?
-        enter ("inferred value " ++ show v ++ " does not match given dot pattern value " ++ show v') $
-          eqVal Pos tv v v'
--}
-
--- checkDot does not need to extract
 -- 2012-01-25 now we do since "extraction" turns also con.terms into records
 checkGoal :: Substitution -> Goal -> TypeCheck ()
 checkGoal subst (DotFlex i me it) = enter ("dot pattern " ++ show me) $
@@ -2754,6 +2734,7 @@
 lowerSemiCont :: Int -> TVal -> TypeCheck Bool
 lowerSemiCont i tv = errorToBool $ lowerSemiContinuous i tv
 
+docNotLowerSemi :: Int -> TVal -> TypeCheck Doc
 docNotLowerSemi i av = text "type " <+> prettyTCM av <+>
   text " not lower semi continuous in " <+> prettyTCM (VGen i)
 
@@ -3013,6 +2994,7 @@
 
       _ -> throwErrorMsg "admPattern: IMPOSSIBLE: pattern for a non-function type"
 
+cannotMatchDeep :: Pattern -> TVal -> TypeCheck ()
 cannotMatchDeep p tv = recoverFailDoc $
   text "cannot match against deep successor pattern"
     <+> text (show p) <+> text "at type" <+> prettyTCM tv
diff --git a/src/Util.hs b/src/Util.hs
--- a/src/Util.hs
+++ b/src/Util.hs
@@ -3,16 +3,20 @@
 {-# LANGUAGE TupleSections, NoMonomorphismRestriction,
       FlexibleInstances, MultiParamTypeClasses, FunctionalDependencies #-}
 
-module Util where
+module Util (module Util, module X) where
 
+-- reexports:
+import Data.List as X (intercalate)
+
 import Prelude hiding (showList, null, (<>))
 
 #if !MIN_VERSION_base(4,8,0)
-import Control.Applicative hiding (empty)
+import Control.Applicative (Applicative, (<$>))
 #endif
 import Control.Monad
 import Control.Monad.Writer (Writer, runWriter)
 
+import qualified Data.List.NonEmpty as List1
 import qualified Data.List as List
 import Data.Map (Map)
 import qualified Data.Map as Map
@@ -20,6 +24,8 @@
 import Debug.Trace
 
 import Text.PrettyPrint as PP
+
+type List1 = List1.NonEmpty
 
 (+?+) :: String -> String -> String
 (+?+) _ "[]" = []
diff --git a/src/Value.hs b/src/Value.hs
--- a/src/Value.hs
+++ b/src/Value.hs
@@ -1,16 +1,20 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE LambdaCase #-}
 {-# LANGUAGE FlexibleContexts, FlexibleInstances, TypeSynonymInstances #-}
 
 module Value where
 
 import Prelude hiding (null)
 
+#if !MIN_VERSION_base(4,8,0)
 import Control.Applicative
-import Control.Monad.Except
+#endif
+import Control.Monad.Except (MonadError)
 
 import qualified Data.List as List
 import Data.Set (Set)
 import qualified Data.Set as Set
-import Debug.Trace
+-- import Debug.Trace
 
 import Abstract
 import Polarity
@@ -73,7 +77,7 @@
 isFun VAbs{}                         = True
 isFun VConst{}                       = True
 isFun (VUp _ VQuant{ vqPiSig = Pi }) = True
-isFun v                              = False
+isFun _                              = False
 
 absName :: FVal -> Name
 absName fv =
@@ -92,7 +96,10 @@
 newtype Valuation = Valuation { valuation :: [(Int,Val)] }
   deriving (Eq,Ord)
 
+emptyVal :: Valuation
 emptyVal  = Valuation []
+
+sgVal :: Int -> Val -> Valuation
 sgVal i v = Valuation [(i,v)]
 
 valuateGen :: Int -> Valuation -> Val
@@ -104,16 +111,11 @@
   { envMap   :: [(Name,a)]          -- the actual map from names to values
   , envBound :: Maybe (Measure Val) -- optionally the current termination measure
   }
-               deriving (Eq,Ord,Show)
+  deriving (Eq, Ord, Show)
 
 type EnvMap = [(Name,Val)]
 type Env = Environ Val
 
-{-
-data MeasVal = MeasVal [Val]  -- lexicographic termination measure
-               deriving (Eq,Ord,Show)
--}
-
 -- smart constructors ------------------------------------------------
 
 -- | The value representing type Size.
@@ -121,6 +123,7 @@
 vSize = VBelow Le VInfty -- 2012-01-28 non-termination bug I have not found
 -- vSize = VSort $ SortC Size
 
+vFinSize :: Val
 vFinSize = VBelow Lt VInfty
 
 -- | Ensure we construct the correct value representing Size.
@@ -133,17 +136,18 @@
 isVSize (VBelow Le VInfty)   = True
 isVSize _                    = False
 
+vTSize :: Val
 vTSize = VSort $ SortC TSize
 
 vTopSort :: Val
 vTopSort = VSort $ Set VInfty
 
 mkClos :: Env -> Expr -> Val
-mkClos rho Infty       = VInfty
-mkClos rho Zero        = VZero
+mkClos _   Infty       = VInfty
+mkClos _   Zero        = VZero
 -- mkClos rho (Succ e)    = VSucc (mkClos rho e)  -- violates an invariant!! succeed/crazys
 mkClos rho (Below ltle e) = VBelow ltle (mkClos rho e)
-mkClos rho (Proj fx n) = VProj fx n
+mkClos _   (Proj fx n) = VProj fx n
 mkClos rho (Var x) = lookupPure rho x
 mkClos rho (Ann e) = mkClos rho $ unTag e
 mkClos rho e = VClos rho e
@@ -151,23 +155,24 @@
   -- VClos (rho { envMap = filterEnv (freeVars e) (envMap rho)}) e
 
 filterEnv :: Set Name -> EnvMap -> EnvMap
-filterEnv ns [] = []
+filterEnv _  [] = []
 filterEnv ns ((x,v) : rho) =
   if Set.member x ns then (x,v) : filterEnv (Set.delete x ns) rho
    else filterEnv ns rho
 
-vDef id   = VDef id `VApp` []
+vDef :: DefId -> Val
+vDef x = VDef x `VApp` []
+
+vCon :: ConK -> QName -> Val
 vCon co n = vDef $ DefId (ConK co) n
 -- vCon co n = vDef $ DefId (ConK (coToConK co)) n
-vFun n    = vDef $ DefId FunK $ QName n
-vDat n    = vDef $ DefId DatK n
 
-{- POSSIBLY BREAKS INVARIANT!
-vApp :: Val -> [Val] -> Val
-vApp f [] = f
-vApp f vs = VApp f vs
--}
+vFun :: Name -> Val
+vFun n = vDef $ DefId FunK $ QName n
 
+vDat :: QName -> Val
+vDat n = vDef $ DefId DatK n
+
 vAbs :: Name -> Int -> Val -> FVal
 vAbs x i v = VAbs x i v emptyVal
 
@@ -175,6 +180,7 @@
 arrow = quant Pi
 prod  = quant Sigma
 
+quant :: PiSigma -> TVal -> Val -> Val
 quant piSig a b = VQuant piSig x (defaultDomain a) (VConst b)
   where x   = fresh ""
 -- quant piSig a b = VQuant piSig x (defaultDomain a) (Environ [(bla,b)] Nothing) (Var bla)
@@ -197,8 +203,8 @@
 -- 1. m
 -- 2. VMax ms  where length ms >= 2 and each mi different
 {- OLD
--- * VSucc^* VGen
--- * VMax vs where each v_i = VSucc^* (VGen k_i) and all k_i different
+-- - VSucc^* VGen
+-- - VMax vs where each v_i = VSucc^* (VGen k_i) and all k_i different
 --           and vs has length >= 2
 -}
 --
@@ -214,14 +220,16 @@
             VMax vs -> maxSize $ map succSize vs
             VMeta i rho n -> VMeta i rho (n + 1)  -- TODO: integrate + and mvar
             _ -> VSucc v
+
+vSucc :: Val -> Val
 vSucc = succSize
 
 -- "multiplication" of sizes
 plusSize :: Val -> Val -> Val
 plusSize VZero v = v
 plusSize v VZero = v
-plusSize VInfty v = VInfty
-plusSize v VInfty = VInfty
+plusSize VInfty _ = VInfty
+plusSize _ VInfty = VInfty
 plusSize (VMax vs) v = maxSize $ map (plusSize v) vs
 plusSize v (VMax vs) = maxSize $ map (plusSize v) vs
 plusSize (VSucc v) v' = succSize $ plusSize v v'
@@ -288,7 +296,7 @@
 
 isDataType :: TVal -> Bool
 isDataType (VApp (VDef (DefId DatK _)) _) = True
-isDataType (VSing v tv) = isDataType tv
+isDataType (VSing _ tv) = isDataType tv
 isDataType _ = False
 
 -- * ugly printing -----------------------------------------------------
@@ -328,7 +336,7 @@
   show (VGuard beta tv) = parens $ show beta ++ " -> " ++ show tv
   show (VBelow ltle v) = show ltle ++ " " ++ show v
 
-  show (VQuant pisig x (Domain (VBelow ltle v) ki dec) bv)
+  show (VQuant pisig x (Domain (VBelow ltle v) _ki dec) bv)
        | (ltle,v) /= (Le,VInfty) =
        parens $ (\ p -> if p==defaultPol then "" else show p) (polarity dec) ++
                 (if erased dec then brackets binding else parens binding)
@@ -351,12 +359,12 @@
   show (VAbs x i v valu) = "(\\" ++ show x ++ "@" ++ show i ++ show v ++ showValuation valu ++ ")"
   show (VUp v vt) = "(" ++ show v ++ " Up " ++ show vt ++ ")"
 
-showSkipLambda v =
-  case v of
-    (VLam x env e)    -> show e ++ showEnv env
-    (VConst v)        -> show v
-    (VAbs x i v valu) -> show v ++ showValuation valu
-    v                 -> show v
+showSkipLambda :: Val -> String
+showSkipLambda = \case
+    (VLam _x env e)     -> show e ++ showEnv env
+    (VConst v)          -> show v
+    (VAbs _x _i v valu) -> show v ++ showValuation valu
+    v                   -> show v
 
 showVals :: [Val] -> String
 showVals [] = ""
diff --git a/src/Version.hs b/src/Version.hs
new file mode 100644
--- /dev/null
+++ b/src/Version.hs
@@ -0,0 +1,13 @@
+-- | Standard module to access version as specified in @.cabal@ file.
+
+module Version ( version ) where
+
+import Data.List    ( intercalate )
+import Data.Version ( Version(versionBranch) )
+
+import qualified Paths_MiniAgda as Paths
+
+-- | The program version obtained from the cabal file.
+
+version :: String
+version = intercalate "." $ map show $ versionBranch Paths.version
diff --git a/src/Warshall.hs b/src/Warshall.hs
--- a/src/Warshall.hs
+++ b/src/Warshall.hs
@@ -83,9 +83,9 @@
 -- constraints ---------------------------------------------------
 
 -- nodes of the graph are either
--- * flexible variables (with identifiers drawn from Int),
--- * rigid variables (also identified by Ints), or
--- * constants (like 0, infinity, or anything between)
+-- - flexible variables (with identifiers drawn from Int),
+-- - rigid variables (also identified by Ints), or
+-- - constants (like 0, infinity, or anything between)
 
 data Node rigid
   = Rigid rigid
diff --git a/stack-8.10.7.yaml b/stack-8.10.7.yaml
new file mode 100644
--- /dev/null
+++ b/stack-8.10.7.yaml
@@ -0,0 +1,4 @@
+resolver: lts-18.28
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/stack-9.0.2.yaml b/stack-9.0.2.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.0.2.yaml
@@ -0,0 +1,4 @@
+resolver: lts-19.3
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/stack-9.10.yaml b/stack-9.10.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.10.yaml
@@ -0,0 +1,4 @@
+resolver: lts-24.1
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/stack-9.12.yaml b/stack-9.12.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.12.yaml
@@ -0,0 +1,5 @@
+resolver: nightly-2025-07-23
+
+extra-deps:
+- haskell-src-exts-1.21.1
+- goldplate-0.2.2.1@rev:2
diff --git a/stack-9.2.5.yaml b/stack-9.2.5.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.2.5.yaml
@@ -0,0 +1,4 @@
+resolver: lts-20.1
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/stack-9.4.3.yaml b/stack-9.4.3.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.4.3.yaml
@@ -0,0 +1,7 @@
+resolver: nightly-2022-11-20
+
+extra-deps:
+- haskell-src-exts-1.21.1
+# temporarily use patched goldplate that uses "/" as path separator also under Windows
+- git: https://github.com/fugue/goldplate.git
+  commit: a671a1dc38d0e73f1598cee5a874d02e520ede71
diff --git a/stack-9.6.yaml b/stack-9.6.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.6.yaml
@@ -0,0 +1,4 @@
+resolver: lts-22.44
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/stack-9.8.yaml b/stack-9.8.yaml
new file mode 100644
--- /dev/null
+++ b/stack-9.8.yaml
@@ -0,0 +1,4 @@
+resolver: lts-23.27
+
+extra-deps:
+- haskell-src-exts-1.21.1
diff --git a/test/GoldplateTests.hs b/test/GoldplateTests.hs
--- a/test/GoldplateTests.hs
+++ b/test/GoldplateTests.hs
@@ -1,5 +1,6 @@
-import System.Exit     ( exitWith  )
-import System.Process  ( system    )
+import System.Environment ( getArgs  )
+import System.Exit        ( exitWith  )
+import System.Process     ( rawSystem )
 
 main :: IO ()
-main = exitWith =<< system ("goldplate test")
+main = exitWith =<< rawSystem "goldplate" . ("test" :) =<< getArgs
diff --git a/test/fail/AccCoqTermination.err b/test/fail/AccCoqTermination.err
--- a/test/fail/AccCoqTermination.err
+++ b/test/fail/AccCoqTermination.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AccCoqTermination.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/AccImplicit.err b/test/fail/AccImplicit.err
--- a/test/fail/AccImplicit.err
+++ b/test/fail/AccImplicit.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AccImplicit.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BadConstraint.err b/test/fail/BadConstraint.err
--- a/test/fail/BadConstraint.err
+++ b/test/fail/BadConstraint.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BadConstraint.ma" ---
 --- scope checking ---
 scope check error: f
diff --git a/test/fail/BadConstraint1.err b/test/fail/BadConstraint1.err
--- a/test/fail/BadConstraint1.err
+++ b/test/fail/BadConstraint1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BadConstraint1.ma" ---
 --- scope checking ---
 scope check error: f
diff --git a/test/fail/BadSizeLambda.err b/test/fail/BadSizeLambda.err
--- a/test/fail/BadSizeLambda.err
+++ b/test/fail/BadSizeLambda.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BadSizeLambda.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BadSizeLambdaCoinductive.err b/test/fail/BadSizeLambdaCoinductive.err
--- a/test/fail/BadSizeLambdaCoinductive.err
+++ b/test/fail/BadSizeLambdaCoinductive.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BadSizeLambdaCoinductive.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BadSizeLambdaInductive.err b/test/fail/BadSizeLambdaInductive.err
--- a/test/fail/BadSizeLambdaInductive.err
+++ b/test/fail/BadSizeLambdaInductive.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BadSizeLambdaInductive.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BigDataInSet0.err b/test/fail/BigDataInSet0.err
--- a/test/fail/BigDataInSet0.err
+++ b/test/fail/BigDataInSet0.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BigDataInSet0.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BoundedFake.err b/test/fail/BoundedFake.err
--- a/test/fail/BoundedFake.err
+++ b/test/fail/BoundedFake.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BoundedFake.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BoundedQStrict.err b/test/fail/BoundedQStrict.err
--- a/test/fail/BoundedQStrict.err
+++ b/test/fail/BoundedQStrict.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BoundedQStrict.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BoundedQWrong.err b/test/fail/BoundedQWrong.err
--- a/test/fail/BoundedQWrong.err
+++ b/test/fail/BoundedQWrong.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BoundedQWrong.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/BoxNeg.err b/test/fail/BoxNeg.err
--- a/test/fail/BoxNeg.err
+++ b/test/fail/BoxNeg.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BoxNeg.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/CheatSubtypingPos.err b/test/fail/CheatSubtypingPos.err
--- a/test/fail/CheatSubtypingPos.err
+++ b/test/fail/CheatSubtypingPos.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "CheatSubtypingPos.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/CoNotLowerSemi.err b/test/fail/CoNotLowerSemi.err
--- a/test/fail/CoNotLowerSemi.err
+++ b/test/fail/CoNotLowerSemi.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "CoNotLowerSemi.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/CoNotLowerSemi1.err b/test/fail/CoNotLowerSemi1.err
--- a/test/fail/CoNotLowerSemi1.err
+++ b/test/fail/CoNotLowerSemi1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "CoNotLowerSemi1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/D.err b/test/fail/D.err
--- a/test/fail/D.err
+++ b/test/fail/D.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "D.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/D1.err b/test/fail/D1.err
--- a/test/fail/D1.err
+++ b/test/fail/D1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "D1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DataAtSetInfty.err b/test/fail/DataAtSetInfty.err
--- a/test/fail/DataAtSetInfty.err
+++ b/test/fail/DataAtSetInfty.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DataAtSetInfty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DeepForcedConstructors.err b/test/fail/DeepForcedConstructors.err
--- a/test/fail/DeepForcedConstructors.err
+++ b/test/fail/DeepForcedConstructors.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DeepForcedConstructors.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DescendAscend.err b/test/fail/DescendAscend.err
--- a/test/fail/DescendAscend.err
+++ b/test/fail/DescendAscend.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DescendAscend.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DescendAscend2.err b/test/fail/DescendAscend2.err
--- a/test/fail/DescendAscend2.err
+++ b/test/fail/DescendAscend2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DescendAscend2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DoNotEraseDataTeleForConTypes.err b/test/fail/DoNotEraseDataTeleForConTypes.err
--- a/test/fail/DoNotEraseDataTeleForConTypes.err
+++ b/test/fail/DoNotEraseDataTeleForConTypes.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DoNotEraseDataTeleForConTypes.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/DottedConstructorsWrong.err b/test/fail/DottedConstructorsWrong.err
--- a/test/fail/DottedConstructorsWrong.err
+++ b/test/fail/DottedConstructorsWrong.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DottedConstructorsWrong.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/EndsCoInEmpty.err b/test/fail/EndsCoInEmpty.err
--- a/test/fail/EndsCoInEmpty.err
+++ b/test/fail/EndsCoInEmpty.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "EndsCoInEmpty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/ExistsSPos.err b/test/fail/ExistsSPos.err
--- a/test/fail/ExistsSPos.err
+++ b/test/fail/ExistsSPos.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ExistsSPos.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/Fib2.err b/test/fail/Fib2.err
--- a/test/fail/Fib2.err
+++ b/test/fail/Fib2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Fib2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/FinBranchMutualWrong.err b/test/fail/FinBranchMutualWrong.err
--- a/test/fail/FinBranchMutualWrong.err
+++ b/test/fail/FinBranchMutualWrong.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "FinBranchMutualWrong.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/FunctionExtensionality.err b/test/fail/FunctionExtensionality.err
--- a/test/fail/FunctionExtensionality.err
+++ b/test/fail/FunctionExtensionality.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "FunctionExtensionality.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/HOMatching.err b/test/fail/HOMatching.err
--- a/test/fail/HOMatching.err
+++ b/test/fail/HOMatching.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HOMatching.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/HetIdFoolingEta.err b/test/fail/HetIdFoolingEta.err
--- a/test/fail/HetIdFoolingEta.err
+++ b/test/fail/HetIdFoolingEta.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HetIdFoolingEta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/HungryEtaRecord.err b/test/fail/HungryEtaRecord.err
--- a/test/fail/HungryEtaRecord.err
+++ b/test/fail/HungryEtaRecord.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HungryEtaRecord.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/IdFoolingEta.err b/test/fail/IdFoolingEta.err
--- a/test/fail/IdFoolingEta.err
+++ b/test/fail/IdFoolingEta.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IdFoolingEta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/IllegalParameter.err b/test/fail/IllegalParameter.err
--- a/test/fail/IllegalParameter.err
+++ b/test/fail/IllegalParameter.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IllegalParameter.ma" ---
 --- scope checking ---
 scope check error: D
diff --git a/test/fail/InconsistentHypotheses.err b/test/fail/InconsistentHypotheses.err
--- a/test/fail/InconsistentHypotheses.err
+++ b/test/fail/InconsistentHypotheses.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "InconsistentHypotheses.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/InjDataLoop.err b/test/fail/InjDataLoop.err
--- a/test/fail/InjDataLoop.err
+++ b/test/fail/InjDataLoop.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "InjDataLoop.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/InjDataLoop2.err b/test/fail/InjDataLoop2.err
--- a/test/fail/InjDataLoop2.err
+++ b/test/fail/InjDataLoop2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "InjDataLoop2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/InvalidField.err b/test/fail/InvalidField.err
--- a/test/fail/InvalidField.err
+++ b/test/fail/InvalidField.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "InvalidField.ma" ---
 --- scope checking ---
 scope check error: D
diff --git a/test/fail/InvalidSizeP.err b/test/fail/InvalidSizeP.err
--- a/test/fail/InvalidSizeP.err
+++ b/test/fail/InvalidSizeP.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "InvalidSizeP.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/IrrHeterogeneousEta.err b/test/fail/IrrHeterogeneousEta.err
--- a/test/fail/IrrHeterogeneousEta.err
+++ b/test/fail/IrrHeterogeneousEta.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IrrHeterogeneousEta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/IrrHeterogeneousFun.err b/test/fail/IrrHeterogeneousFun.err
--- a/test/fail/IrrHeterogeneousFun.err
+++ b/test/fail/IrrHeterogeneousFun.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IrrHeterogeneousFun.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MeasureInTelescope.err b/test/fail/MeasureInTelescope.err
--- a/test/fail/MeasureInTelescope.err
+++ b/test/fail/MeasureInTelescope.err
@@ -1,3 +1,2 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasureInTelescope.ma" ---
 --- scope checking ---
diff --git a/test/fail/MeasureInValue.err b/test/fail/MeasureInValue.err
--- a/test/fail/MeasureInValue.err
+++ b/test/fail/MeasureInValue.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasureInValue.ma" ---
 --- scope checking ---
 scope check error: f
diff --git a/test/fail/MeasuresTypo.err b/test/fail/MeasuresTypo.err
--- a/test/fail/MeasuresTypo.err
+++ b/test/fail/MeasuresTypo.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasuresTypo.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MixedMeasureLength.err b/test/fail/MixedMeasureLength.err
--- a/test/fail/MixedMeasureLength.err
+++ b/test/fail/MixedMeasureLength.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MixedMeasureLength.ma" ---
 --- scope checking ---
 scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length
diff --git a/test/fail/MixedMeasuredUnmeasured.err b/test/fail/MixedMeasuredUnmeasured.err
--- a/test/fail/MixedMeasuredUnmeasured.err
+++ b/test/fail/MixedMeasuredUnmeasured.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MixedMeasuredUnmeasured.ma" ---
 --- scope checking ---
 scope check error: in a mutual function block, either all functions must be without measure or have a measure of the same length
diff --git a/test/fail/MuOnlyPosNotSPos.err b/test/fail/MuOnlyPosNotSPos.err
--- a/test/fail/MuOnlyPosNotSPos.err
+++ b/test/fail/MuOnlyPosNotSPos.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MuOnlyPosNotSPos.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MustBeCofun.err b/test/fail/MustBeCofun.err
--- a/test/fail/MustBeCofun.err
+++ b/test/fail/MustBeCofun.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MustBeCofun.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MutualDataNotMon.err b/test/fail/MutualDataNotMon.err
--- a/test/fail/MutualDataNotMon.err
+++ b/test/fail/MutualDataNotMon.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MutualDataNotMon.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MutualNeg.err b/test/fail/MutualNeg.err
--- a/test/fail/MutualNeg.err
+++ b/test/fail/MutualNeg.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MutualNeg.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/MutualNeg2.err b/test/fail/MutualNeg2.err
--- a/test/fail/MutualNeg2.err
+++ b/test/fail/MutualNeg2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MutualNeg2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NatToSize.err b/test/fail/NatToSize.err
--- a/test/fail/NatToSize.err
+++ b/test/fail/NatToSize.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NatToSize.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NegPol.err b/test/fail/NegPol.err
--- a/test/fail/NegPol.err
+++ b/test/fail/NegPol.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NegPol.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NonLinearParameter.err b/test/fail/NonLinearParameter.err
--- a/test/fail/NonLinearParameter.err
+++ b/test/fail/NonLinearParameter.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NonLinearParameter.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NonLinearParameterPattern.err b/test/fail/NonLinearParameterPattern.err
--- a/test/fail/NonLinearParameterPattern.err
+++ b/test/fail/NonLinearParameterPattern.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NonLinearParameterPattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NonLinearPatterns.err b/test/fail/NonLinearPatterns.err
--- a/test/fail/NonLinearPatterns.err
+++ b/test/fail/NonLinearPatterns.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NonLinearPatterns.ma" ---
 --- scope checking ---
 scope check error: nonlin
diff --git a/test/fail/NonPosBoundedData.err b/test/fail/NonPosBoundedData.err
--- a/test/fail/NonPosBoundedData.err
+++ b/test/fail/NonPosBoundedData.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NonPosBoundedData.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NotEnoughParameters.err b/test/fail/NotEnoughParameters.err
--- a/test/fail/NotEnoughParameters.err
+++ b/test/fail/NotEnoughParameters.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NotEnoughParameters.ma" ---
 --- scope checking ---
 scope check error: D
diff --git a/test/fail/NotForcedConstructors.err b/test/fail/NotForcedConstructors.err
--- a/test/fail/NotForcedConstructors.err
+++ b/test/fail/NotForcedConstructors.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NotForcedConstructors.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/NumbersAsIds.err b/test/fail/NumbersAsIds.err
--- a/test/fail/NumbersAsIds.err
+++ b/test/fail/NumbersAsIds.err
@@ -1,3 +1,2 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NumbersAsIds.ma" ---
 --- scope checking ---
diff --git a/test/fail/OverlappingPatternIndFam-sound.err b/test/fail/OverlappingPatternIndFam-sound.err
--- a/test/fail/OverlappingPatternIndFam-sound.err
+++ b/test/fail/OverlappingPatternIndFam-sound.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "OverlappingPatternIndFam-sound.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/OverlappingPatternIndFam.err b/test/fail/OverlappingPatternIndFam.err
--- a/test/fail/OverlappingPatternIndFam.err
+++ b/test/fail/OverlappingPatternIndFam.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "OverlappingPatternIndFam.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/PolarityWrongCast.err b/test/fail/PolarityWrongCast.err
--- a/test/fail/PolarityWrongCast.err
+++ b/test/fail/PolarityWrongCast.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "PolarityWrongCast.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/RecurseOnErased.err b/test/fail/RecurseOnErased.err
--- a/test/fail/RecurseOnErased.err
+++ b/test/fail/RecurseOnErased.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "RecurseOnErased.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/ResurrectFromErasedPattern.err b/test/fail/ResurrectFromErasedPattern.err
--- a/test/fail/ResurrectFromErasedPattern.err
+++ b/test/fail/ResurrectFromErasedPattern.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ResurrectFromErasedPattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/SPosNotPos.err b/test/fail/SPosNotPos.err
--- a/test/fail/SPosNotPos.err
+++ b/test/fail/SPosNotPos.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "SPosNotPos.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/ShadowBinding.err b/test/fail/ShadowBinding.err
--- a/test/fail/ShadowBinding.err
+++ b/test/fail/ShadowBinding.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ShadowBinding.ma" ---
 --- scope checking ---
 scope check error: (let A = A in A): Identifier A already in context
diff --git a/test/fail/ShadowParameter.err b/test/fail/ShadowParameter.err
--- a/test/fail/ShadowParameter.err
+++ b/test/fail/ShadowParameter.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ShadowParameter.ma" ---
 --- scope checking ---
 scope check error: Sg
diff --git a/test/fail/ShadowPatternParameter.err b/test/fail/ShadowPatternParameter.err
--- a/test/fail/ShadowPatternParameter.err
+++ b/test/fail/ShadowPatternParameter.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ShadowPatternParameter.ma" ---
 --- scope checking ---
 scope check error: D
diff --git a/test/fail/SizedDataWrongPol.err b/test/fail/SizedDataWrongPol.err
--- a/test/fail/SizedDataWrongPol.err
+++ b/test/fail/SizedDataWrongPol.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "SizedDataWrongPol.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/StoreSize.err b/test/fail/StoreSize.err
--- a/test/fail/StoreSize.err
+++ b/test/fail/StoreSize.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StoreSize.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/StreamDupl.err b/test/fail/StreamDupl.err
--- a/test/fail/StreamDupl.err
+++ b/test/fail/StreamDupl.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StreamDupl.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/StreamNotSemiCont.err b/test/fail/StreamNotSemiCont.err
--- a/test/fail/StreamNotSemiCont.err
+++ b/test/fail/StreamNotSemiCont.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StreamNotSemiCont.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/Tm.err b/test/fail/Tm.err
--- a/test/fail/Tm.err
+++ b/test/fail/Tm.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Tm.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/TypeInTypeViaSetInfty.err b/test/fail/TypeInTypeViaSetInfty.err
--- a/test/fail/TypeInTypeViaSetInfty.err
+++ b/test/fail/TypeInTypeViaSetInfty.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "TypeInTypeViaSetInfty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/UlfsCounterexample.err b/test/fail/UlfsCounterexample.err
--- a/test/fail/UlfsCounterexample.err
+++ b/test/fail/UlfsCounterexample.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "UlfsCounterexample.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/UlfsCounterexample2.err b/test/fail/UlfsCounterexample2.err
--- a/test/fail/UlfsCounterexample2.err
+++ b/test/fail/UlfsCounterexample2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "UlfsCounterexample2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/VectorPatternNotForced.err b/test/fail/VectorPatternNotForced.err
--- a/test/fail/VectorPatternNotForced.err
+++ b/test/fail/VectorPatternNotForced.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "VectorPatternNotForced.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/VeiledParameter.err b/test/fail/VeiledParameter.err
--- a/test/fail/VeiledParameter.err
+++ b/test/fail/VeiledParameter.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "VeiledParameter.ma" ---
 --- scope checking ---
 scope check error: D
diff --git a/test/fail/absurdPatUnit.err b/test/fail/absurdPatUnit.err
--- a/test/fail/absurdPatUnit.err
+++ b/test/fail/absurdPatUnit.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "absurdPatUnit.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/adm/adm1.err b/test/fail/adm/adm1.err
--- a/test/fail/adm/adm1.err
+++ b/test/fail/adm/adm1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "adm/adm1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/adm/adm2.err b/test/fail/adm/adm2.err
--- a/test/fail/adm/adm2.err
+++ b/test/fail/adm/adm2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "adm/adm2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/adm/adm3.err b/test/fail/adm/adm3.err
--- a/test/fail/adm/adm3.err
+++ b/test/fail/adm/adm3.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "adm/adm3.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/bfSizePatternIncomplete.err b/test/fail/bfSizePatternIncomplete.err
--- a/test/fail/bfSizePatternIncomplete.err
+++ b/test/fail/bfSizePatternIncomplete.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "bfSizePatternIncomplete.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/bfTypeNotAdmissible.err b/test/fail/bfTypeNotAdmissible.err
--- a/test/fail/bfTypeNotAdmissible.err
+++ b/test/fail/bfTypeNotAdmissible.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "bfTypeNotAdmissible.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/bigData.err b/test/fail/bigData.err
--- a/test/fail/bigData.err
+++ b/test/fail/bigData.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "bigData.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/coSetOmega.err b/test/fail/coSetOmega.err
--- a/test/fail/coSetOmega.err
+++ b/test/fail/coSetOmega.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "coSetOmega.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/coSizeInFun.err b/test/fail/coSizeInFun.err
--- a/test/fail/coSizeInFun.err
+++ b/test/fail/coSizeInFun.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "coSizeInFun.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/codataNotMonotone.err b/test/fail/codataNotMonotone.err
--- a/test/fail/codataNotMonotone.err
+++ b/test/fail/codataNotMonotone.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "codataNotMonotone.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/codyPatternConditionExplicit.err b/test/fail/codyPatternConditionExplicit.err
--- a/test/fail/codyPatternConditionExplicit.err
+++ b/test/fail/codyPatternConditionExplicit.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "codyPatternConditionExplicit.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/codyPatternConditionExplicit2.err b/test/fail/codyPatternConditionExplicit2.err
--- a/test/fail/codyPatternConditionExplicit2.err
+++ b/test/fail/codyPatternConditionExplicit2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "codyPatternConditionExplicit2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/cofunIntoBoolTimesStream.err b/test/fail/cofunIntoBoolTimesStream.err
--- a/test/fail/cofunIntoBoolTimesStream.err
+++ b/test/fail/cofunIntoBoolTimesStream.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "cofunIntoBoolTimesStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/cofunIntoStreamPlusStream.err b/test/fail/cofunIntoStreamPlusStream.err
--- a/test/fail/cofunIntoStreamPlusStream.err
+++ b/test/fail/cofunIntoStreamPlusStream.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "cofunIntoStreamPlusStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/countingBT.err b/test/fail/countingBT.err
--- a/test/fail/countingBT.err
+++ b/test/fail/countingBT.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "countingBT.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/countingMerge.err b/test/fail/countingMerge.err
--- a/test/fail/countingMerge.err
+++ b/test/fail/countingMerge.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "countingMerge.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/dataNotMonotone.err b/test/fail/dataNotMonotone.err
--- a/test/fail/dataNotMonotone.err
+++ b/test/fail/dataNotMonotone.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "dataNotMonotone.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/drop.err b/test/fail/drop.err
--- a/test/fail/drop.err
+++ b/test/fail/drop.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "drop.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/erased1.err b/test/fail/erased1.err
--- a/test/fail/erased1.err
+++ b/test/fail/erased1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "erased1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/f_x_is_f_0.err b/test/fail/f_x_is_f_0.err
--- a/test/fail/f_x_is_f_0.err
+++ b/test/fail/f_x_is_f_0.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "f_x_is_f_0.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/fail1.err b/test/fail/fail1.err
--- a/test/fail/fail1.err
+++ b/test/fail/fail1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "fail1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/fibStream.err b/test/fail/fibStream.err
--- a/test/fail/fibStream.err
+++ b/test/fail/fibStream.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "fibStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/hang.err b/test/fail/hang.err
--- a/test/fail/hang.err
+++ b/test/fail/hang.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "hang.ma" ---
 --- scope checking ---
 scope check error: f
diff --git a/test/fail/hang2.err b/test/fail/hang2.err
--- a/test/fail/hang2.err
+++ b/test/fail/hang2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "hang2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/huetHullotReverse.err b/test/fail/huetHullotReverse.err
--- a/test/fail/huetHullotReverse.err
+++ b/test/fail/huetHullotReverse.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "huetHullotReverse.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/incompleteSizePattern1.err b/test/fail/incompleteSizePattern1.err
--- a/test/fail/incompleteSizePattern1.err
+++ b/test/fail/incompleteSizePattern1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "incompleteSizePattern1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/incompleteSizePattern2.err b/test/fail/incompleteSizePattern2.err
--- a/test/fail/incompleteSizePattern2.err
+++ b/test/fail/incompleteSizePattern2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "incompleteSizePattern2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/inconsistentAssumption.err b/test/fail/inconsistentAssumption.err
--- a/test/fail/inconsistentAssumption.err
+++ b/test/fail/inconsistentAssumption.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "inconsistentAssumption.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/inconsistentAssumption2.err b/test/fail/inconsistentAssumption2.err
--- a/test/fail/inconsistentAssumption2.err
+++ b/test/fail/inconsistentAssumption2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "inconsistentAssumption2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/inductiveNotDotPattern.err b/test/fail/inductiveNotDotPattern.err
--- a/test/fail/inductiveNotDotPattern.err
+++ b/test/fail/inductiveNotDotPattern.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "inductiveNotDotPattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/lengthCoList.err b/test/fail/lengthCoList.err
--- a/test/fail/lengthCoList.err
+++ b/test/fail/lengthCoList.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "lengthCoList.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/lengthCoList2.err b/test/fail/lengthCoList2.err
--- a/test/fail/lengthCoList2.err
+++ b/test/fail/lengthCoList2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "lengthCoList2.ma" ---
 --- scope checking ---
 scope check error: convert3
diff --git a/test/fail/loop.err b/test/fail/loop.err
--- a/test/fail/loop.err
+++ b/test/fail/loop.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loop.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopAdmStream-Nat.err b/test/fail/loopAdmStream-Nat.err
--- a/test/fail/loopAdmStream-Nat.err
+++ b/test/fail/loopAdmStream-Nat.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopAdmStream-Nat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopAdmStream-simplified.err b/test/fail/loopAdmStream-simplified.err
--- a/test/fail/loopAdmStream-simplified.err
+++ b/test/fail/loopAdmStream-simplified.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopAdmStream-simplified.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopAdmStream.err b/test/fail/loopAdmStream.err
--- a/test/fail/loopAdmStream.err
+++ b/test/fail/loopAdmStream.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopAdmStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopBadTypesHidden.err b/test/fail/loopBadTypesHidden.err
--- a/test/fail/loopBadTypesHidden.err
+++ b/test/fail/loopBadTypesHidden.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopBadTypesHidden.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopBounded.err b/test/fail/loopBounded.err
--- a/test/fail/loopBounded.err
+++ b/test/fail/loopBounded.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopBounded.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopOldNoSizePattern.err b/test/fail/loopOldNoSizePattern.err
--- a/test/fail/loopOldNoSizePattern.err
+++ b/test/fail/loopOldNoSizePattern.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopOldNoSizePattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/loopTypesHiddenInData.err b/test/fail/loopTypesHiddenInData.err
--- a/test/fail/loopTypesHiddenInData.err
+++ b/test/fail/loopTypesHiddenInData.err
@@ -1,3 +1,2 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "loopTypesHiddenInData.ma" ---
 --- scope checking ---
diff --git a/test/fail/mapStream2.err b/test/fail/mapStream2.err
--- a/test/fail/mapStream2.err
+++ b/test/fail/mapStream2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "mapStream2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/mapStream2sizeMatchDepth2.err b/test/fail/mapStream2sizeMatchDepth2.err
--- a/test/fail/mapStream2sizeMatchDepth2.err
+++ b/test/fail/mapStream2sizeMatchDepth2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "mapStream2sizeMatchDepth2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/matchOnNatSuccI.err b/test/fail/matchOnNatSuccI.err
--- a/test/fail/matchOnNatSuccI.err
+++ b/test/fail/matchOnNatSuccI.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "matchOnNatSuccI.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/match_erased.err b/test/fail/match_erased.err
--- a/test/fail/match_erased.err
+++ b/test/fail/match_erased.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "match_erased.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/match_on_set.err b/test/fail/match_on_set.err
--- a/test/fail/match_on_set.err
+++ b/test/fail/match_on_set.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "match_on_set.ma" ---
 --- scope checking ---
 scope check error: bla
diff --git a/test/fail/negativeFam.err b/test/fail/negativeFam.err
--- a/test/fail/negativeFam.err
+++ b/test/fail/negativeFam.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "negativeFam.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/notAdmMonotoneArg.err b/test/fail/notAdmMonotoneArg.err
--- a/test/fail/notAdmMonotoneArg.err
+++ b/test/fail/notAdmMonotoneArg.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "notAdmMonotoneArg.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/omegaInst.err b/test/fail/omegaInst.err
--- a/test/fail/omegaInst.err
+++ b/test/fail/omegaInst.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "omegaInst.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/omegaInst1.err b/test/fail/omegaInst1.err
--- a/test/fail/omegaInst1.err
+++ b/test/fail/omegaInst1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "omegaInst1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/onesStreamUnguarded.err b/test/fail/onesStreamUnguarded.err
--- a/test/fail/onesStreamUnguarded.err
+++ b/test/fail/onesStreamUnguarded.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "onesStreamUnguarded.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/partialFunction.err b/test/fail/partialFunction.err
--- a/test/fail/partialFunction.err
+++ b/test/fail/partialFunction.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "partialFunction.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/relevantArgErasedMagicVec.err b/test/fail/relevantArgErasedMagicVec.err
--- a/test/fail/relevantArgErasedMagicVec.err
+++ b/test/fail/relevantArgErasedMagicVec.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "relevantArgErasedMagicVec.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/scolist_not_lsc1.err b/test/fail/scolist_not_lsc1.err
--- a/test/fail/scolist_not_lsc1.err
+++ b/test/fail/scolist_not_lsc1.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "scolist_not_lsc1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/scolist_not_lsc2.err b/test/fail/scolist_not_lsc2.err
--- a/test/fail/scolist_not_lsc2.err
+++ b/test/fail/scolist_not_lsc2.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "scolist_not_lsc2.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/shadowGlobal.err b/test/fail/shadowGlobal.err
--- a/test/fail/shadowGlobal.err
+++ b/test/fail/shadowGlobal.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "shadowGlobal.ma" ---
 --- scope checking ---
 scope check error: "shadowing of global definitions forbidden": Identifier bla already in signature
diff --git a/test/fail/shouldBeDotPattern_snat.err b/test/fail/shouldBeDotPattern_snat.err
--- a/test/fail/shouldBeDotPattern_snat.err
+++ b/test/fail/shouldBeDotPattern_snat.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "shouldBeDotPattern_snat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/singleton.err b/test/fail/singleton.err
--- a/test/fail/singleton.err
+++ b/test/fail/singleton.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "singleton.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/sizePatternSucc.err b/test/fail/sizePatternSucc.err
--- a/test/fail/sizePatternSucc.err
+++ b/test/fail/sizePatternSucc.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizePatternSucc.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/stream.err b/test/fail/stream.err
--- a/test/fail/stream.err
+++ b/test/fail/stream.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "stream.ma" ---
 --- scope checking ---
 scope check error: Stream
diff --git a/test/fail/streamMisc.err b/test/fail/streamMisc.err
--- a/test/fail/streamMisc.err
+++ b/test/fail/streamMisc.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "streamMisc.ma" ---
 --- scope checking ---
 scope check error: wkStream2
diff --git a/test/fail/stream_x_is_cons_x_tail_x.err b/test/fail/stream_x_is_cons_x_tail_x.err
--- a/test/fail/stream_x_is_cons_x_tail_x.err
+++ b/test/fail/stream_x_is_cons_x_tail_x.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "stream_x_is_cons_x_tail_x.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/subtyping_erased.err b/test/fail/subtyping_erased.err
--- a/test/fail/subtyping_erased.err
+++ b/test/fail/subtyping_erased.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "subtyping_erased.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/subtyping_erased_wrongdir.err b/test/fail/subtyping_erased_wrongdir.err
--- a/test/fail/subtyping_erased_wrongdir.err
+++ b/test/fail/subtyping_erased_wrongdir.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "subtyping_erased_wrongdir.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/swapVariablesWithoutDecrease.err b/test/fail/swapVariablesWithoutDecrease.err
--- a/test/fail/swapVariablesWithoutDecrease.err
+++ b/test/fail/swapVariablesWithoutDecrease.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "swapVariablesWithoutDecrease.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/tailBad.err b/test/fail/tailBad.err
--- a/test/fail/tailBad.err
+++ b/test/fail/tailBad.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "tailBad.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/vec_eta.err b/test/fail/vec_eta.err
--- a/test/fail/vec_eta.err
+++ b/test/fail/vec_eta.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "vec_eta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/fail/vec_length.err b/test/fail/vec_length.err
--- a/test/fail/vec_length.err
+++ b/test/fail/vec_length.err
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "vec_length.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/should-fail/AgdaIssue1015.golden b/test/should-fail/AgdaIssue1015.golden
--- a/test/should-fail/AgdaIssue1015.golden
+++ b/test/should-fail/AgdaIssue1015.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AgdaIssue1015.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/should-fail/AgdaIssue1015NonMutual.golden b/test/should-fail/AgdaIssue1015NonMutual.golden
--- a/test/should-fail/AgdaIssue1015NonMutual.golden
+++ b/test/should-fail/AgdaIssue1015NonMutual.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AgdaIssue1015NonMutual.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/should-fail/StrictInfty.golden b/test/should-fail/StrictInfty.golden
--- a/test/should-fail/StrictInfty.golden
+++ b/test/should-fail/StrictInfty.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StrictInfty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/should-succeed/Umlaut.err b/test/should-succeed/Umlaut.err
--- a/test/should-succeed/Umlaut.err
+++ b/test/should-succeed/Umlaut.err
@@ -1,3 +1,2 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Umlaut.ma" ---
 --- scope checking ---
diff --git a/test/succeed/AbsurdMatchNonLin.golden b/test/succeed/AbsurdMatchNonLin.golden
--- a/test/succeed/AbsurdMatchNonLin.golden
+++ b/test/succeed/AbsurdMatchNonLin.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AbsurdMatchNonLin.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/AccDestructorErasedIndex.golden b/test/succeed/AccDestructorErasedIndex.golden
--- a/test/succeed/AccDestructorErasedIndex.golden
+++ b/test/succeed/AccDestructorErasedIndex.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AccDestructorErasedIndex.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/AgdaIssue1052.golden b/test/succeed/AgdaIssue1052.golden
--- a/test/succeed/AgdaIssue1052.golden
+++ b/test/succeed/AgdaIssue1052.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AgdaIssue1052.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/AgdaIssue1055.golden b/test/succeed/AgdaIssue1055.golden
--- a/test/succeed/AgdaIssue1055.golden
+++ b/test/succeed/AgdaIssue1055.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AgdaIssue1055.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/AppendAddSize.golden b/test/succeed/AppendAddSize.golden
--- a/test/succeed/AppendAddSize.golden
+++ b/test/succeed/AppendAddSize.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "AppendAddSize.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/BelowLeInfty.golden b/test/succeed/BelowLeInfty.golden
--- a/test/succeed/BelowLeInfty.golden
+++ b/test/succeed/BelowLeInfty.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BelowLeInfty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/BigWrap.golden b/test/succeed/BigWrap.golden
--- a/test/succeed/BigWrap.golden
+++ b/test/succeed/BigWrap.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BigWrap.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/BoundedQ.golden b/test/succeed/BoundedQ.golden
--- a/test/succeed/BoundedQ.golden
+++ b/test/succeed/BoundedQ.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BoundedQ.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/BuiltinSigma.golden b/test/succeed/BuiltinSigma.golden
--- a/test/succeed/BuiltinSigma.golden
+++ b/test/succeed/BuiltinSigma.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "BuiltinSigma.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/CoFunReturnsProduct.golden b/test/succeed/CoFunReturnsProduct.golden
--- a/test/succeed/CoFunReturnsProduct.golden
+++ b/test/succeed/CoFunReturnsProduct.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "CoFunReturnsProduct.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ConorMcBrideCalco09inflationary.golden b/test/succeed/ConorMcBrideCalco09inflationary.golden
--- a/test/succeed/ConorMcBrideCalco09inflationary.golden
+++ b/test/succeed/ConorMcBrideCalco09inflationary.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ConorMcBrideCalco09inflationary.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ConstructorTelescopes.golden b/test/succeed/ConstructorTelescopes.golden
--- a/test/succeed/ConstructorTelescopes.golden
+++ b/test/succeed/ConstructorTelescopes.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ConstructorTelescopes.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ConstructorVeiledTarget.golden b/test/succeed/ConstructorVeiledTarget.golden
--- a/test/succeed/ConstructorVeiledTarget.golden
+++ b/test/succeed/ConstructorVeiledTarget.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ConstructorVeiledTarget.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DataTypesNotFamilies.golden b/test/succeed/DataTypesNotFamilies.golden
--- a/test/succeed/DataTypesNotFamilies.golden
+++ b/test/succeed/DataTypesNotFamilies.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DataTypesNotFamilies.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DeepMatch.golden b/test/succeed/DeepMatch.golden
--- a/test/succeed/DeepMatch.golden
+++ b/test/succeed/DeepMatch.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DeepMatch.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DescendAscendTerm.golden b/test/succeed/DescendAscendTerm.golden
--- a/test/succeed/DescendAscendTerm.golden
+++ b/test/succeed/DescendAscendTerm.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DescendAscendTerm.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DotPatternNotLeftToRightBinding.golden b/test/succeed/DotPatternNotLeftToRightBinding.golden
--- a/test/succeed/DotPatternNotLeftToRightBinding.golden
+++ b/test/succeed/DotPatternNotLeftToRightBinding.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DotPatternNotLeftToRightBinding.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DottedConstructors.golden b/test/succeed/DottedConstructors.golden
--- a/test/succeed/DottedConstructors.golden
+++ b/test/succeed/DottedConstructors.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DottedConstructors.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/DottedPatSyn.golden b/test/succeed/DottedPatSyn.golden
--- a/test/succeed/DottedPatSyn.golden
+++ b/test/succeed/DottedPatSyn.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "DottedPatSyn.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Empty.golden b/test/succeed/Empty.golden
--- a/test/succeed/Empty.golden
+++ b/test/succeed/Empty.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Empty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/EvalBoveCaprettaNotSized.golden b/test/succeed/EvalBoveCaprettaNotSized.golden
--- a/test/succeed/EvalBoveCaprettaNotSized.golden
+++ b/test/succeed/EvalBoveCaprettaNotSized.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "EvalBoveCaprettaNotSized.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/EvenOdd.golden b/test/succeed/EvenOdd.golden
--- a/test/succeed/EvenOdd.golden
+++ b/test/succeed/EvenOdd.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "EvenOdd.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Evens.golden b/test/succeed/Evens.golden
--- a/test/succeed/Evens.golden
+++ b/test/succeed/Evens.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Evens.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ExtractLets.golden b/test/succeed/ExtractLets.golden
--- a/test/succeed/ExtractLets.golden
+++ b/test/succeed/ExtractLets.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ExtractLets.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/FakeMutual.golden b/test/succeed/FakeMutual.golden
--- a/test/succeed/FakeMutual.golden
+++ b/test/succeed/FakeMutual.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "FakeMutual.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Fields.golden b/test/succeed/Fields.golden
--- a/test/succeed/Fields.golden
+++ b/test/succeed/Fields.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Fields.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/FinBranchMutual.golden b/test/succeed/FinBranchMutual.golden
--- a/test/succeed/FinBranchMutual.golden
+++ b/test/succeed/FinBranchMutual.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "FinBranchMutual.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Fix.golden b/test/succeed/Fix.golden
--- a/test/succeed/Fix.golden
+++ b/test/succeed/Fix.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Fix.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ForceInConType.golden b/test/succeed/ForceInConType.golden
--- a/test/succeed/ForceInConType.golden
+++ b/test/succeed/ForceInConType.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ForceInConType.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ForcedMatch.golden b/test/succeed/ForcedMatch.golden
--- a/test/succeed/ForcedMatch.golden
+++ b/test/succeed/ForcedMatch.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ForcedMatch.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ForcedMatchIdType.golden b/test/succeed/ForcedMatchIdType.golden
--- a/test/succeed/ForcedMatchIdType.golden
+++ b/test/succeed/ForcedMatchIdType.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ForcedMatchIdType.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ForestRose.golden b/test/succeed/ForestRose.golden
--- a/test/succeed/ForestRose.golden
+++ b/test/succeed/ForestRose.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ForestRose.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/GADT.golden b/test/succeed/GADT.golden
--- a/test/succeed/GADT.golden
+++ b/test/succeed/GADT.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "GADT.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/GoodConstraint.golden b/test/succeed/GoodConstraint.golden
--- a/test/succeed/GoodConstraint.golden
+++ b/test/succeed/GoodConstraint.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "GoodConstraint.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/HEq.golden b/test/succeed/HEq.golden
--- a/test/succeed/HEq.golden
+++ b/test/succeed/HEq.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HEq.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/HVec.golden b/test/succeed/HVec.golden
--- a/test/succeed/HVec.golden
+++ b/test/succeed/HVec.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HVec.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/HungryEtaRecord.golden b/test/succeed/HungryEtaRecord.golden
--- a/test/succeed/HungryEtaRecord.golden
+++ b/test/succeed/HungryEtaRecord.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "HungryEtaRecord.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/IdTypePos.golden b/test/succeed/IdTypePos.golden
--- a/test/succeed/IdTypePos.golden
+++ b/test/succeed/IdTypePos.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IdTypePos.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/IrrHeterogeneousFun.golden b/test/succeed/IrrHeterogeneousFun.golden
--- a/test/succeed/IrrHeterogeneousFun.golden
+++ b/test/succeed/IrrHeterogeneousFun.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IrrHeterogeneousFun.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/IrrHeterogeneousSingleton.golden b/test/succeed/IrrHeterogeneousSingleton.golden
--- a/test/succeed/IrrHeterogeneousSingleton.golden
+++ b/test/succeed/IrrHeterogeneousSingleton.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IrrHeterogeneousSingleton.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/IrrHeterogeneousSize.golden b/test/succeed/IrrHeterogeneousSize.golden
--- a/test/succeed/IrrHeterogeneousSize.golden
+++ b/test/succeed/IrrHeterogeneousSize.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "IrrHeterogeneousSize.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/LargeElim.golden b/test/succeed/LargeElim.golden
--- a/test/succeed/LargeElim.golden
+++ b/test/succeed/LargeElim.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "LargeElim.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/LetTele.golden b/test/succeed/LetTele.golden
--- a/test/succeed/LetTele.golden
+++ b/test/succeed/LetTele.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "LetTele.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/LowerSemiCont.golden b/test/succeed/LowerSemiCont.golden
--- a/test/succeed/LowerSemiCont.golden
+++ b/test/succeed/LowerSemiCont.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "LowerSemiCont.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MeasureInFunTele.golden b/test/succeed/MeasureInFunTele.golden
--- a/test/succeed/MeasureInFunTele.golden
+++ b/test/succeed/MeasureInFunTele.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasureInFunTele.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MeasuredHerSubst1.golden b/test/succeed/MeasuredHerSubst1.golden
--- a/test/succeed/MeasuredHerSubst1.golden
+++ b/test/succeed/MeasuredHerSubst1.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasuredHerSubst1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MeasuredRose.golden b/test/succeed/MeasuredRose.golden
--- a/test/succeed/MeasuredRose.golden
+++ b/test/succeed/MeasuredRose.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MeasuredRose.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MergeWith.golden b/test/succeed/MergeWith.golden
--- a/test/succeed/MergeWith.golden
+++ b/test/succeed/MergeWith.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MergeWith.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MockSig.golden b/test/succeed/MockSig.golden
--- a/test/succeed/MockSig.golden
+++ b/test/succeed/MockSig.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MockSig.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Mu.golden b/test/succeed/Mu.golden
--- a/test/succeed/Mu.golden
+++ b/test/succeed/Mu.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Mu.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MultiSigma.golden b/test/succeed/MultiSigma.golden
--- a/test/succeed/MultiSigma.golden
+++ b/test/succeed/MultiSigma.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MultiSigma.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MutualBigDataKindInf.golden b/test/succeed/MutualBigDataKindInf.golden
--- a/test/succeed/MutualBigDataKindInf.golden
+++ b/test/succeed/MutualBigDataKindInf.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MutualBigDataKindInf.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/MutualRecordsNoEta.golden b/test/succeed/MutualRecordsNoEta.golden
--- a/test/succeed/MutualRecordsNoEta.golden
+++ b/test/succeed/MutualRecordsNoEta.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "MutualRecordsNoEta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Nested.golden b/test/succeed/Nested.golden
--- a/test/succeed/Nested.golden
+++ b/test/succeed/Nested.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Nested.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/NewSyntaxTour.golden b/test/succeed/NewSyntaxTour.golden
--- a/test/succeed/NewSyntaxTour.golden
+++ b/test/succeed/NewSyntaxTour.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "NewSyntaxTour.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Nisse2012-02-17.golden b/test/succeed/Nisse2012-02-17.golden
--- a/test/succeed/Nisse2012-02-17.golden
+++ b/test/succeed/Nisse2012-02-17.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Nisse2012-02-17.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Nisse2012-03-06.golden b/test/succeed/Nisse2012-03-06.golden
--- a/test/succeed/Nisse2012-03-06.golden
+++ b/test/succeed/Nisse2012-03-06.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Nisse2012-03-06.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/OverloadedConstructors.golden b/test/succeed/OverloadedConstructors.golden
--- a/test/succeed/OverloadedConstructors.golden
+++ b/test/succeed/OverloadedConstructors.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "OverloadedConstructors.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/PTSRule.golden b/test/succeed/PTSRule.golden
--- a/test/succeed/PTSRule.golden
+++ b/test/succeed/PTSRule.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "PTSRule.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ParseMultBind.golden b/test/succeed/ParseMultBind.golden
--- a/test/succeed/ParseMultBind.golden
+++ b/test/succeed/ParseMultBind.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ParseMultBind.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ParsePipeOperators.golden b/test/succeed/ParsePipeOperators.golden
--- a/test/succeed/ParsePipeOperators.golden
+++ b/test/succeed/ParsePipeOperators.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ParsePipeOperators.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Pattern.golden b/test/succeed/Pattern.golden
--- a/test/succeed/Pattern.golden
+++ b/test/succeed/Pattern.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Pattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/PatternParameters.golden b/test/succeed/PatternParameters.golden
--- a/test/succeed/PatternParameters.golden
+++ b/test/succeed/PatternParameters.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "PatternParameters.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Polarities.golden b/test/succeed/Polarities.golden
--- a/test/succeed/Polarities.golden
+++ b/test/succeed/Polarities.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Polarities.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/PredDepType.golden b/test/succeed/PredDepType.golden
--- a/test/succeed/PredDepType.golden
+++ b/test/succeed/PredDepType.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "PredDepType.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Prelude.golden b/test/succeed/Prelude.golden
--- a/test/succeed/Prelude.golden
+++ b/test/succeed/Prelude.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Prelude.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Prod.golden b/test/succeed/Prod.golden
--- a/test/succeed/Prod.golden
+++ b/test/succeed/Prod.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Prod.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Projections.golden b/test/succeed/Projections.golden
--- a/test/succeed/Projections.golden
+++ b/test/succeed/Projections.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Projections.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Rose.golden b/test/succeed/Rose.golden
--- a/test/succeed/Rose.golden
+++ b/test/succeed/Rose.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Rose.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/SP.golden b/test/succeed/SP.golden
--- a/test/succeed/SP.golden
+++ b/test/succeed/SP.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "SP.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ScopeCheckFunDef.golden b/test/succeed/ScopeCheckFunDef.golden
--- a/test/succeed/ScopeCheckFunDef.golden
+++ b/test/succeed/ScopeCheckFunDef.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ScopeCheckFunDef.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/SgPredWrongMon.golden b/test/succeed/SgPredWrongMon.golden
--- a/test/succeed/SgPredWrongMon.golden
+++ b/test/succeed/SgPredWrongMon.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "SgPredWrongMon.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/SolverBugStreamFixed.golden b/test/succeed/SolverBugStreamFixed.golden
--- a/test/succeed/SolverBugStreamFixed.golden
+++ b/test/succeed/SolverBugStreamFixed.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "SolverBugStreamFixed.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Squash.golden b/test/succeed/Squash.golden
--- a/test/succeed/Squash.golden
+++ b/test/succeed/Squash.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Squash.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Stack.golden b/test/succeed/Stack.golden
--- a/test/succeed/Stack.golden
+++ b/test/succeed/Stack.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Stack.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/StreamDupl.golden b/test/succeed/StreamDupl.golden
--- a/test/succeed/StreamDupl.golden
+++ b/test/succeed/StreamDupl.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StreamDupl.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/StrictBoundedQCoinductive.golden b/test/succeed/StrictBoundedQCoinductive.golden
--- a/test/succeed/StrictBoundedQCoinductive.golden
+++ b/test/succeed/StrictBoundedQCoinductive.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "StrictBoundedQCoinductive.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/UPolyList.golden b/test/succeed/UPolyList.golden
--- a/test/succeed/UPolyList.golden
+++ b/test/succeed/UPolyList.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "UPolyList.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/Universe.golden b/test/succeed/Universe.golden
--- a/test/succeed/Universe.golden
+++ b/test/succeed/Universe.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "Universe.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/VecNotErased.golden b/test/succeed/VecNotErased.golden
--- a/test/succeed/VecNotErased.golden
+++ b/test/succeed/VecNotErased.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "VecNotErased.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/WrapAbsurd.golden b/test/succeed/WrapAbsurd.golden
--- a/test/succeed/WrapAbsurd.golden
+++ b/test/succeed/WrapAbsurd.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "WrapAbsurd.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/absurdPattern.golden b/test/succeed/absurdPattern.golden
--- a/test/succeed/absurdPattern.golden
+++ b/test/succeed/absurdPattern.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "absurdPattern.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/addWith.golden b/test/succeed/addWith.golden
--- a/test/succeed/addWith.golden
+++ b/test/succeed/addWith.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "addWith.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/casePair.golden b/test/succeed/casePair.golden
--- a/test/succeed/casePair.golden
+++ b/test/succeed/casePair.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "casePair.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/caseSList.golden b/test/succeed/caseSList.golden
--- a/test/succeed/caseSList.golden
+++ b/test/succeed/caseSList.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "caseSList.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/conat.golden b/test/succeed/conat.golden
--- a/test/succeed/conat.golden
+++ b/test/succeed/conat.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "conat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/countConstructors.golden b/test/succeed/countConstructors.golden
--- a/test/succeed/countConstructors.golden
+++ b/test/succeed/countConstructors.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "countConstructors.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/crazys.golden b/test/succeed/crazys.golden
--- a/test/succeed/crazys.golden
+++ b/test/succeed/crazys.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "crazys.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/drop.golden b/test/succeed/drop.golden
--- a/test/succeed/drop.golden
+++ b/test/succeed/drop.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "drop.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/eta.golden b/test/succeed/eta.golden
--- a/test/succeed/eta.golden
+++ b/test/succeed/eta.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "eta.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/eta_unit.golden b/test/succeed/eta_unit.golden
--- a/test/succeed/eta_unit.golden
+++ b/test/succeed/eta_unit.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "eta_unit.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/exists.golden b/test/succeed/exists.golden
--- a/test/succeed/exists.golden
+++ b/test/succeed/exists.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "exists.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/fib.golden b/test/succeed/fib.golden
--- a/test/succeed/fib.golden
+++ b/test/succeed/fib.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "fib.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/fibDeep.golden b/test/succeed/fibDeep.golden
--- a/test/succeed/fibDeep.golden
+++ b/test/succeed/fibDeep.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "fibDeep.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/gcd-either.golden b/test/succeed/gcd-either.golden
--- a/test/succeed/gcd-either.golden
+++ b/test/succeed/gcd-either.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "gcd-either.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/hamming.golden b/test/succeed/hamming.golden
--- a/test/succeed/hamming.golden
+++ b/test/succeed/hamming.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "hamming.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/ho.golden b/test/succeed/ho.golden
--- a/test/succeed/ho.golden
+++ b/test/succeed/ho.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "ho.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/implicitSizeVarUsedExplicitely.golden b/test/succeed/implicitSizeVarUsedExplicitely.golden
--- a/test/succeed/implicitSizeVarUsedExplicitely.golden
+++ b/test/succeed/implicitSizeVarUsedExplicitely.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "implicitSizeVarUsedExplicitely.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/lengthCoList.golden b/test/succeed/lengthCoList.golden
--- a/test/succeed/lengthCoList.golden
+++ b/test/succeed/lengthCoList.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "lengthCoList.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/list.golden b/test/succeed/list.golden
--- a/test/succeed/list.golden
+++ b/test/succeed/list.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "list.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/logic.golden b/test/succeed/logic.golden
--- a/test/succeed/logic.golden
+++ b/test/succeed/logic.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "logic.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/lossyIdentityOnStreams.golden b/test/succeed/lossyIdentityOnStreams.golden
--- a/test/succeed/lossyIdentityOnStreams.golden
+++ b/test/succeed/lossyIdentityOnStreams.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "lossyIdentityOnStreams.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/magicVecLookupProofIrr.golden b/test/succeed/magicVecLookupProofIrr.golden
--- a/test/succeed/magicVecLookupProofIrr.golden
+++ b/test/succeed/magicVecLookupProofIrr.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "magicVecLookupProofIrr.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/mapStream.golden b/test/succeed/mapStream.golden
--- a/test/succeed/mapStream.golden
+++ b/test/succeed/mapStream.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "mapStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/max.golden b/test/succeed/max.golden
--- a/test/succeed/max.golden
+++ b/test/succeed/max.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "max.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/measures.golden b/test/succeed/measures.golden
--- a/test/succeed/measures.golden
+++ b/test/succeed/measures.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "measures.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/msort-implicit.golden b/test/succeed/msort-implicit.golden
--- a/test/succeed/msort-implicit.golden
+++ b/test/succeed/msort-implicit.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "msort-implicit.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/msort.golden b/test/succeed/msort.golden
--- a/test/succeed/msort.golden
+++ b/test/succeed/msort.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "msort.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/nat.golden b/test/succeed/nat.golden
--- a/test/succeed/nat.golden
+++ b/test/succeed/nat.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "nat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/non-record.golden b/test/succeed/non-record.golden
--- a/test/succeed/non-record.golden
+++ b/test/succeed/non-record.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "non-record.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/old_stream.golden b/test/succeed/old_stream.golden
--- a/test/succeed/old_stream.golden
+++ b/test/succeed/old_stream.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "old_stream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/oldnat.golden b/test/succeed/oldnat.golden
--- a/test/succeed/oldnat.golden
+++ b/test/succeed/oldnat.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "oldnat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/omegaInst1.golden b/test/succeed/omegaInst1.golden
--- a/test/succeed/omegaInst1.golden
+++ b/test/succeed/omegaInst1.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "omegaInst1.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/omegaInstTailInfty.golden b/test/succeed/omegaInstTailInfty.golden
--- a/test/succeed/omegaInstTailInfty.golden
+++ b/test/succeed/omegaInstTailInfty.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "omegaInstTailInfty.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/pred.golden b/test/succeed/pred.golden
--- a/test/succeed/pred.golden
+++ b/test/succeed/pred.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "pred.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/qsapp.golden b/test/succeed/qsapp.golden
--- a/test/succeed/qsapp.golden
+++ b/test/succeed/qsapp.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "qsapp.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/quicksort-filter-fragment.golden b/test/succeed/quicksort-filter-fragment.golden
--- a/test/succeed/quicksort-filter-fragment.golden
+++ b/test/succeed/quicksort-filter-fragment.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "quicksort-filter-fragment.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/quicksort-filter.golden b/test/succeed/quicksort-filter.golden
--- a/test/succeed/quicksort-filter.golden
+++ b/test/succeed/quicksort-filter.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "quicksort-filter.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/quicksort.golden b/test/succeed/quicksort.golden
--- a/test/succeed/quicksort.golden
+++ b/test/succeed/quicksort.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "quicksort.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/rank2SizeQuantStream.golden b/test/succeed/rank2SizeQuantStream.golden
--- a/test/succeed/rank2SizeQuantStream.golden
+++ b/test/succeed/rank2SizeQuantStream.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "rank2SizeQuantStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/record.golden b/test/succeed/record.golden
--- a/test/succeed/record.golden
+++ b/test/succeed/record.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "record.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/shadowDataParam.golden b/test/succeed/shadowDataParam.golden
--- a/test/succeed/shadowDataParam.golden
+++ b/test/succeed/shadowDataParam.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "shadowDataParam.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sigma.golden b/test/succeed/sigma.golden
--- a/test/succeed/sigma.golden
+++ b/test/succeed/sigma.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sigma.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/simple_nat.golden b/test/succeed/simple_nat.golden
--- a/test/succeed/simple_nat.golden
+++ b/test/succeed/simple_nat.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "simple_nat.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/singleton.golden b/test/succeed/singleton.golden
--- a/test/succeed/singleton.golden
+++ b/test/succeed/singleton.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "singleton.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sizeFunctions.golden b/test/succeed/sizeFunctions.golden
--- a/test/succeed/sizeFunctions.golden
+++ b/test/succeed/sizeFunctions.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizeFunctions.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sizedFinitelyBranchingTrees.golden b/test/succeed/sizedFinitelyBranchingTrees.golden
--- a/test/succeed/sizedFinitelyBranchingTrees.golden
+++ b/test/succeed/sizedFinitelyBranchingTrees.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizedFinitelyBranchingTrees.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sizedMax.golden b/test/succeed/sizedMax.golden
--- a/test/succeed/sizedMax.golden
+++ b/test/succeed/sizedMax.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizedMax.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sizedMergeWith.golden b/test/succeed/sizedMergeWith.golden
--- a/test/succeed/sizedMergeWith.golden
+++ b/test/succeed/sizedMergeWith.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizedMergeWith.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/sizedOrd.golden b/test/succeed/sizedOrd.golden
--- a/test/succeed/sizedOrd.golden
+++ b/test/succeed/sizedOrd.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "sizedOrd.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/streamIdentityNatRecursive.golden b/test/succeed/streamIdentityNatRecursive.golden
--- a/test/succeed/streamIdentityNatRecursive.golden
+++ b/test/succeed/streamIdentityNatRecursive.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "streamIdentityNatRecursive.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/subset.golden b/test/succeed/subset.golden
--- a/test/succeed/subset.golden
+++ b/test/succeed/subset.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "subset.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/tailStream.golden b/test/succeed/tailStream.golden
--- a/test/succeed/tailStream.golden
+++ b/test/succeed/tailStream.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "tailStream.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/vec.golden b/test/succeed/vec.golden
--- a/test/succeed/vec.golden
+++ b/test/succeed/vec.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "vec.ma" ---
 --- scope checking ---
 --- type checking ---
diff --git a/test/succeed/wkStream.golden b/test/succeed/wkStream.golden
--- a/test/succeed/wkStream.golden
+++ b/test/succeed/wkStream.golden
@@ -1,4 +1,3 @@
-MiniAgda by Andreas Abel and Karl Mehltretter
 --- opening "wkStream.ma" ---
 --- scope checking ---
 --- type checking ---