diff --git a/AbsSynToTerm.hs b/AbsSynToTerm.hs
--- a/AbsSynToTerm.hs
+++ b/AbsSynToTerm.hs
@@ -73,11 +73,7 @@
                           
    (A.EAbs _ _ _) -> throwError "cannot use lambda for type"
    _              -> Pi (Irr dummyVar) <$> resolveTerm a <*> local (insertVar dummyVar) (resolveTerm b)
-{-
- where o = case arrow of                     
-         A.Arrow "=>" -> Pr
-         A.Arrow "->" -> Ty
--}
+
 resolveTerm (A.EAbs ids _arrow_ b) = manyLam ids b
 resolveTerm (A.EPair (A.Decl (A.AIdent i) e) rest) = Pair (Irr i) <$> resolveTerm e <*> local (insertVar i) (resolveTerm rest)
 resolveTerm (A.EAnn e1 e2) = Ann <$> resolveTerm e1 <*> resolveTerm e2
diff --git a/Main.hs b/Main.hs
--- a/Main.hs
+++ b/Main.hs
@@ -64,25 +64,11 @@
     Right (a,b) -> do 
        putStrV 0 $ "nf =" <+> pretty a
        putStrV 0 $ "ty =" <+> pretty b
-{-
-       case b of 
-         (Pi i s t) -> do
-           putStrV v $ "s ∈ ⟦S⟧ =" <+> prettyTerm (S.singleton i) (zerInRel s)
-           putStrV v $ "T =" <+> prettyTerm (S.singleton i) t
-         _ -> putStrV v "not a function!"
--}
        return True
     Left (e,err) -> do let Irr (line,col) = termPosition e 
                        putStrV 0 (text fname <> ":" <> pretty line <> ":" <> pretty (col - 1) <> ":" <+> err)
                        return False
       
-{-
-showTree tree
- = do
-      putStrV 2 $ "\n[Abstract Syntax]\n\n" ++ show tree
-      putStrV 2 $ "\n[Linearized tree]\n\n" ++ printTree tree
--}
-
 main :: IO ()
 main = do 
   results <- mapM runFile (files options)
diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -30,17 +30,12 @@
      
      Sigma :: Ident -> NF -> NF -> NF
      Pair  :: Ident -> NF -> NF -> NF  -- Pair does not bind any variable.
-     Proj  :: -- ^ Sort of the argument (only needed for
-                           -- the 1st projection: 2nd projection does
-                           -- not change relevance)
-              Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.
+     Proj  :: Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.
               Irr String -> Neutral 
      
-     
      V :: Int -> Variable -- deBruijn index 
      Hole :: String -> Variable
 
-
 type Subst = [NF]
 
 deriving instance Eq (Term n)
@@ -49,17 +44,12 @@
 var :: Int -> NF
 var x = Neu $ var' x
 
-var'' = V 
-
 var' x = Var $ V x
 
-
 -- | Hereditary substitution
 subst0 :: NF -> NF -> NF
 subst0 u = subst (u:map (var) [0..])  
 
-showShift (Sort l) = replicate l '^' 
-
 subst :: Subst -> Term n -> NF
 subst f t = case t of
   Neu x -> s x
@@ -80,10 +70,12 @@
        s  = subst f
 
 
+-- | Hereditary application
 app :: NF -> NF -> NF 
 app (Lam i _ bo) u = subst0 u bo
 app (Neu n)      u = Neu (App n u)
 
+-- | Hereditary projection
 proj :: NF -> Bool -> Irr String -> NF
 proj (Pair _ x y) True f = x
 proj (Pair _ x y) False f = y
diff --git a/Terms.hs b/Terms.hs
--- a/Terms.hs
+++ b/Terms.hs
@@ -47,84 +47,6 @@
 termPosition (Extr x _) = termPosition x
 termPosition (Ann x _) = termPosition x
 
-{-
-bound = Bound dummyPosition
-
--- | Hereditary application
--- invariant: preserves normal forms 
-app :: Term -> Term -> Term 
-app (Lam i _ bo) u = subst0 u bo
-app neutral u = neutral :$: u
-
-subst0 :: Term -> Term -> Term
-subst0 u = subst (u:map bound [0..])  
-
-type Subst = [Term]
-
-
-
--- | Hereditary substitution
-subst :: Subst -> Term -> Term
-subst f t = case t of
-  Bound _ x -> f !! x
-  Lam i ty bo -> Lam i (s ty) (s' bo)
-  Pi i a b -> Pi i (s a) (s' b)
-  Sigma i a b -> Sigma i (s a) (s' b)
-  (a :$: b) -> (s a) `app` (s b)
-  (Ann e t) -> Ann (s e) (s t)
-  (Pair i x y) -> Pair i (s x) (s' y)
-  (Proj x f) -> proj (s x) f
-  (Extr x f) -> extr (s x) f
-  Hole p x -> Hole p x
-  Star p x -> Star p x
-  Param arity x -> param0 arity (s x)
-  OfParam i x -> OfParam i (s x)
-  Shift f x -> ssubst f (s x)
-  Destroy i x -> Destroy i (s x) -- need to move to sort annotated terms to do this correctly. 
-  
- where s' = subst (bound 0 : map wk f)
-       s  = subst f
-
--- | Non-hereditary substitution
-subst' :: Subst -> Term -> Term
-subst' f t = case t of
-  Bound _ x -> f !! x
-  Lam i ty bo -> Lam i (s ty) (s' bo)
-  Pi i a b -> Pi i (s a) (s' b)
-  Sigma i a b -> Sigma i (s a) (s' b)
-  (a :$: b) -> (s a) `app` (s b)
-  (Ann e t) -> Ann (s e) (s t)
-  (Pair i x y) -> Pair i (s x) (s' y)
-  (Proj x f) -> Proj (s x) f
-  (Extr x f) -> Extr (s x) f
-  Hole p x -> Hole p x
-  Star p x -> Star p x
-  Param arity x -> Param arity (s x)
-  OfParam i x -> OfParam i (s x)
-  Shift f x -> Shift f (s x)
-  Destroy i x -> Destroy i (s x)
-  
- where s' = subst (bound 0 : map wk f)
-       s  = subst f
-
-
-wkn n = subst' (map bound [n..])
-wk = wkn 1
-str = subst0 (Hole dummyPosition "oops!")
-
--- | Hereditary projection
-proj (Extr x f')   f | f /= f' = proj x f
-proj (Pair (Irr (Identifier (_pos,f'))) x y) f 
-  | f == f' = x
-   | f /= f' = proj (str y) f
-proj x f = Proj x f
-
--- | Hereditary extraction
-extr (Pair (Irr (Identifier (_pos,f'))) x y) f | f == f' = str y
-extr x f = Extr x f
-
--}
-
 deriving instance Show (Term)
 deriving instance Eq (Term)
 
@@ -185,152 +107,3 @@
 instance Pretty Term where
     pretty = prettyTerm mempty
 
-{-
----------------------------------------------------------------
--- Sort substitution
-
-ssubst :: Sort -> Term -> Term
-ssubst f t = case t of
-  Bound p x -> Shift f (Bound p x)
-  Lam i ty bo -> Lam i (s ty) (s bo)
-  Pi i a b -> Pi i (s a) (s b)
-  Sigma i a b -> Sigma i (s a) (s b)
-  (a :$: b) -> (s a) :$: (s b)
-  (Ann e t) -> Ann (s e) (s t)
-  (Pair i x y) -> Pair i (s x) (s y)
-  (Proj x f) -> Proj (s x) f
-  (Extr x f) -> Extr (s x) f
-  Hole p x -> Hole p x
-  Star p x -> Star p (f + x)
-  Param arity x -> Param arity (s x)
-  OfParam i x -> OfParam (modId (++ show f) i) (s x)  
-  Shift f' x -> ssubst (f + f') x
-  Destroy f x -> Destroy f (s x)
- where s = ssubst f
-
----------------------------------------------------------------
--- Hereditary parametricity transform
-
-type Env = [Subst]
-
-renam :: Env -> Int -> Term -> Term
-renam g idx a = ssubst nextRel $ subst (g !! idx) a
-
-re :: Int -> Ident -> Ident
-re idx = modId (++ subscriptShow idx)
-
-param0 arity = param arity (map (Param arity . bound) [0..] : replicate arity (map bound [0..]))
-
--- | Transform a term to its relational interpretation
-param :: Int -> Env -> Term -> Term
-param arity = paramProg
-  where
-  extCtx gs = [bound idx:map (wkn (arity + 1)) g | (idx,g) <- zip (0:reverse [1..arity]) gs]
-    
-  paramProg :: Env -> Term -> Term
-  paramProg g (Shift f x) = Shift f (paramProg g x) 
-  paramProg g (Destroy f x) = Param arity (Destroy f x)
-  paramProg g (Hole p s) = Hole p ("[" ++ s ++ "]")
-  paramProg g (Bound p x) = g !! 0 !! x
-  paramProg g (Lam i ty bo) = paramBind g Lam  i ty $
-                          paramProg (extCtx g) bo
-    
-  paramProg g (Pair i x y) = 
-     Pair i (paramProg g x) 
-            (paramProg (map (\d -> Hole dummyPosition "pair not in nf!":map wk d) g) y)
-     -- because the input is in normal form, the variable bound by the
-     -- pair can never appear in y.
-  paramProg g (f :$: a) = foldl app (paramProg g f) [renam g idx a | idx <- [1..arity]] `app` paramProg g a
-  paramProg g (Proj e f) = proj (paramProg g e) f
-  paramProg g (Extr e f) = extr (paramProg g e) f
-  paramProg g (Ann _ _) = error "Ann should not be in nf term"
-  paramProg g (OfParam i x) = case arity of
-      0 -> OfParam (modId (\x -> "⌈" ++ x ++ "⌉") i) (paramProg g x)                                
-      1 -> x `app` ssubst nextRel (OfParam i x) 
-      _ -> error "mismatch in arity not yet supported"
-  paramProg g x@(Param _ _) = Param arity x -- FIXME: here the renaming substitution should be applied;
-                              -- but applying the current substitution has the effect of swapping the params.
-  paramProg g ty = appl [Lam (synthId $ "z" ++ subscriptShow i) (wkn (i-1) $ renam g i ty) | i <- [1..arity] ] (zerInRel g ty)
-
-  appl :: [a -> a] -> a -> a
-  appl []     x = x
-  appl (f:fs) x = f (appl fs x)
-
-  -- | Build a relation witnessing x ∈ ⟦ty⟧. (where 'x' is not bound in 'ty'.)
-  zerInRel :: Env -> Term -> Term
-  zerInRel gs ty = inParam (map (map (wkn arity)) gs) ty (reverse $ map bound [0..arity-1])
-
-  -- | Build a relation z ∈ ⟦ty⟧.  z is a term that, after renaming,
-  -- gives the vector of terms member of the relation.  Note that
-  -- 'param' is never applied to 'z', therefore 'zR' never occurs in the result.
-
-  inParam :: Env -> Term -> [Term] -> Term
-  inParam g (Star  p s)   zs = appl [Pi dummyId (wkn i z) | (i,z) <- zip [0..] zs] (Star p s)
-  inParam g (Pi    i a b) zs = paramBind g Pi i a (inParam (extCtx g) b 
-                                                  [(wkn (arity + 1) z `app` bound i) | (i,z) <- zip (reverse [1..arity]) zs])
-
-  inParam g@(g0:gs) (Sigma name@(Irr (Identifier (_,f))) a b) zs = 
-    Sigma name (inParam g a (map (`proj` f) zs))
-    (inParam ((bound 0:map wk g0):[(proj (wk z) f):map wk g2 | (g2,z) <- zip gs zs]) b [(Extr (wk z) f) | z <- zs])
-  -- z ∈ ⟦(x : A) × B(x)⟧ =   (x : π₁ z ∈ ⟦A⟧) × π₂ z ∈ ⟦B(x)⟧
-
-  inParam g (Sigma _ _ _) z = error "Σ not implemented"
-  inParam g t z = foldl app (paramProg g t) z
-
-  -- | Translate a binding (x : A) into (x₁ : A₁) (⟦x⟧ : ⟦A⟧ x₁)
-  paramBind :: Env -> (Ident -> Term -> Term -> Term) -> Ident -> Term -> Term -> Term
-  paramBind g binder name a rest = 
-      appl 
-      [binder (re i name) (wkn (i-1) $ renam g i a) | i <- [1..arity]] $
-      binder name         (zerInRel g a) $ 
-      rest 
-
-nextRel = Sort 0 1
-nxt = ssubst nextRel
-
---------------------------
--- destruction of worlds
-
-
-destruction :: Int -> Seq Bool -> Term -> Maybe Term
-destruction destroyed d t = case t of
-  (Hole p x)  -> Just $ Hole p ("|" ++  x ++ "|")
-  (Bound p x)  
-    | x >= Data.Sequence.length d -> Just (Bound p x)  
-    -- FIXME: this is incorrect; instead the callers of this function
-    -- must give the correct value for variables of the environment.
-    | otherwise -> if d `index` x then Just (Bound p x) else Nothing
-  (Star p (Sort l w))  
-      | w >= destroyed -> Nothing
-  (Star p (Sort l r))  -> Just $ Star p (Sort l r)
-  (Pi i a b)  -> mb d Pi i a b 
-  (Sigma i a b)  -> mb d Sigma i a b 
-  (Lam i ty bo)  -> mb d Lam i ty bo  
-  (Pair i a b)  -> mb d Pair i a b 
-  (Ann e t)  -> Ann <$> pr e <*> pr t 
-  (a :$: b)  -> case pr b of
-                   Nothing -> pr a
-                   Just b' -> (:$: b') <$> pr a 
-  (Proj x f) -> (\x -> Proj x f) <$> pr x  
-  (Extr x f) -> (\x -> Extr x f) <$> pr x  
-  
-  -- FIXME: This should traverse the potential series of Param to find if the variable is removed.
-  (Param arity (Bound p x)) | x < Data.Sequence.length d && not (d `index` x) -> Nothing
-  -- Just a "renaming" on NFs: x should be a (renamed) variable.
-  (Param arity x) -> Just (Destroy destroyed (Param arity x))
-  (Shift f x)    ->  Just (Destroy destroyed (Shift f x))
-   
-  (OfParam n x) -> OfParam (modId (++ "%" ++ show destroyed) n) <$> pr x
-  
-
- where mb d binder i a b = case pr a of
-                             Nothing -> str <$> destruction destroyed (False <| d) b
-                             Just a' -> binder i a' <$> destruction destroyed (True <| d) b
-       pr x = destruction destroyed d x
-
--- pr (Param x) d = Just x FIXME: there is a problem here: 1st
--- order variables have been removed, so we cannot refer to them.
-
-
-  
--}
diff --git a/TypeCheckerNF.hs b/TypeCheckerNF.hs
--- a/TypeCheckerNF.hs
+++ b/TypeCheckerNF.hs
@@ -91,7 +91,7 @@
 iType g e@(Terms.Bound _ x) = do
   return $ (val $ value, wkn (x+1) $ typ)
   where val (Direct v) = wkn (x+1) v
-        val _ = var x -- etaExpand o (var' x) typ
+        val _ = var x -- We could do eta-expansion here: etaExpand (var' x) typ
         Bind _ value typ = g `index` x
         
 iType g (Terms.Hole p x) = do
@@ -140,7 +140,7 @@
          return $ (hole h, Sort 1)
     _ -> throwError (e,displayT g e <+> "is not a type")
 
-
+-- | Test if two types are equal.
 unify :: Context -> Term -> Type -> Type -> Result ()
 unify g e q q' =
          do let ii = length g
diff --git a/nanoAgda.cabal b/nanoAgda.cabal
--- a/nanoAgda.cabal
+++ b/nanoAgda.cabal
@@ -1,5 +1,5 @@
 name:           nanoAgda
-version:        0.1.0
+version:        0.1.1
 category:       Dependent Types
 synopsis:       A toy dependently-typed language
 description:
@@ -16,7 +16,7 @@
 author:         Jean-Philippe Bernardy
 maintainer:     jeanphilippe.bernardy@gmail.com
 Cabal-Version:  >= 1.8
-tested-with:    GHC==6.12.3
+tested-with:    GHC==7.2.2
 build-type:     Simple
 
 executable nanoAgda