diff --git a/Normal.hs b/Normal.hs
--- a/Normal.hs
+++ b/Normal.hs
@@ -11,30 +11,26 @@
 
 data No
 data Ne
-data Va
 
 type NF = Term No
 type Neutral = Term Ne
-type Variable = Term Va
-type NF' = (NF, NF) -- value, type.
 
 data Term n :: * where
      Neu :: Neutral -> NF
-     Var :: Variable -> Neutral
-     
-     Star :: Sort -> NF     
+     Star :: Sort -> NF
      
      Pi  :: Ident -> NF -> NF -> NF
      Lam :: Ident -> NF -> NF -> NF 
-     App :: Neutral -> NF -> Neutral -- The sort is that of the argument.
+     App :: Neutral -> NF -> Neutral
      
      Sigma :: Ident -> NF -> NF -> NF
      Pair  :: Ident -> NF -> NF -> NF  -- Pair does not bind any variable.
      Proj  :: Neutral -> Bool -> -- ^ True for 1st projection; False for 2nd.
               Irr String -> Neutral 
      
-     V :: Int -> Variable -- deBruijn index 
-     Hole :: String -> Variable
+     V :: Int ->  -- ^ deBruijn index 
+          Neutral
+     Hole :: String -> Neutral
 
 type Subst = [NF]
 
@@ -42,9 +38,7 @@
 deriving instance Show (Term n)
 
 var :: Int -> NF
-var x = Neu $ var' x
-
-var' x = Var $ V x
+var x = Neu $ V x
 
 -- | Hereditary substitution
 subst0 :: NF -> NF -> NF
@@ -53,18 +47,15 @@
 subst :: Subst -> Term n -> NF
 subst f t = case t of
   Neu x -> s x
-  Var x -> s x
-  
   Star x -> Star x
-  
   Lam i ty bo -> Lam i (s ty) (s' bo)
-  (Pair i x y) -> Pair i (s x) (s y)
+  Pair i x y -> Pair i (s x) (s y)
   Pi i a b -> Pi i (s a) (s' b)
   Sigma i a b -> Sigma i (s a) (s' b)
   (App a b) -> app (s a) (s b)
   (Proj x k f) -> proj (s x) k f
-  Hole x -> Neu $ Var $ Hole x
-  V x -> (f !! x)
+  Hole x -> Neu $ Hole x
+  V x -> f !! x
  where s,s' :: forall n. Term n -> NF
        s' = subst (var 0 : map wk f)
        s  = subst f
@@ -81,20 +72,16 @@
 proj (Pair _ x y) False f = y
 proj (Neu x) k f = Neu (Proj x k f)
 
+hole = Neu . Hole
 
+-- | Weakening
 wkn :: Int -> NF -> NF
 wkn n = subst (map var [n..])
 
-wkdn :: Int -> Int -> NF -> NF
-wkdn d n = subst (map var [0..d-1] ++ map var [d+n..])
-
 wk = wkn 1
-str = subst0 (Neu $ Var $ Hole "str: oops!")
 
-wkv :: Int -> Variable -> Variable
-wkv n (V x) = V (x + n)
-wkv n (Hole x) = Hole x
-
+-- | Inverse of weakening
+str = subst0 (Neu $ Hole "str: oops!")
 
 -----------------------------------
 -- Display
@@ -102,7 +89,6 @@
 dec xs = [ x - 1 | x <- xs, x > 0]
 
 freeVars :: Term n -> [Int]
-freeVars (Var x) = freeVars x
 freeVars (Neu x) = freeVars x
 freeVars (Pi _ a b) = freeVars a <> (dec $ freeVars b)
 freeVars (Sigma _ a b) = freeVars a <> (dec $ freeVars b)
@@ -123,7 +109,6 @@
   | otherwise = s
 
 cPrint :: Int -> DisplayContext -> Term n -> Doc
-cPrint p ii (Var x) = cPrint p ii x
 cPrint p ii (Neu x) = cPrint p ii x
 cPrint p ii (Hole x) = text x
 cPrint p ii (Star i) = pretty i
diff --git a/Terms.hs b/Terms.hs
--- a/Terms.hs
+++ b/Terms.hs
@@ -34,6 +34,7 @@
      -- Type annotation. Not present in normal forms.
      Ann :: Term -> Term -> Term 
      
+-- | Position of a term, for error-reporting
 termPosition :: Term -> Irr Position 
 termPosition (Hole p _) = p
 termPosition (Star p _) = p
diff --git a/TypeCheckerNF.hs b/TypeCheckerNF.hs
--- a/TypeCheckerNF.hs
+++ b/TypeCheckerNF.hs
@@ -10,6 +10,8 @@
 --
 -- are also used for this implementation.
 --
+-- Additionally, this implementation performs evaluation to normal
+-- form and type checking/inference at the same time.
 
 module TypeCheckerNF where
 
@@ -69,8 +71,7 @@
 
 -- FIXME: flag an error if impredicativity disabled and we use it anyway.
 
-hole = Neu . Var . Hole
-
+-- | Infer a type and evaluate to normal form
 iType :: Context -> Term -> Result (Value,Type)
 iType g (Ann e tyt)
   =     do  (ty,o) <- iSort g tyt 
@@ -91,7 +92,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 -- We could do eta-expansion here: etaExpand (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
@@ -130,12 +131,13 @@
     (ve,t) <- iType (Bind x Abstract vty <| g) e
     return $ (Lam x vty ve, Pi x vty t)
 
+-- | Infer a sort, and normalise
 iSort :: Context -> Term -> Result (Type,Sort)
 iSort g e = do
   (val,v) <- iType g e
   case v of 
     Star i -> return (val,i)
-    (Neu (Var (Hole h))) -> do 
+    (Neu (Hole h)) -> do 
          report $ text h <+> "must be a type"
          return $ (hole h, Sort 1)
     _ -> throwError (e,displayT g e <+> "is not a type")
@@ -147,8 +149,8 @@
                 constraint = report $ vcat ["constraint: " <> display g q',
                                             "equal to  : " <> display g q]
             case (q,q') of
-              ((Neu (Var (Hole _))), t) -> constraint
-              (t, Neu (Var (Hole _))) -> constraint
+              ((Neu (Hole _)), t) -> constraint
+              (t, Neu (Hole _)) -> constraint
               _ -> unless (q == q') 
                        (throwError (e,hang "type mismatch: " 2 $ vcat 
                                              ["inferred:" <+> display g q',
@@ -156,7 +158,7 @@
                                               "for:" <+> displayT g e ,
                                               "context:" <+> dispContext g]))
 
--- Check the type and normalize
+-- | Check the type and normalize
 cType :: Context -> Term -> Type -> Result Value
 cType g (Terms.Lam name (Terms.Hole _ _) e) (Pi name' ty ty') = do
         e' <- cType (Bind name Abstract ty <| g) e ty'
diff --git a/nanoAgda.cabal b/nanoAgda.cabal
--- a/nanoAgda.cabal
+++ b/nanoAgda.cabal
@@ -1,5 +1,5 @@
 name:           nanoAgda
-version:        0.1.1
+version:        1.0.0
 category:       Dependent Types
 synopsis:       A toy dependently-typed language
 description:
@@ -39,7 +39,7 @@
   build-depends: containers==0.4.*
   build-depends: pretty==1.1.*
   build-depends: parsec==2.1.*
-  build-depends: BNFC-meta==0.2.*
+  build-depends: BNFC-meta==0.3.*
   build-depends: transformers == 0.2.*
   build-depends: mtl == 2.0.*