change words

src/Kind/Check.hs

@@ -33,7 +33,7 @@ infer src term dep = debug ("infer: " ++ termShower False term dep) $ go src ter
         envSusp (Check Nothing arg ftyp_inp dep)
         return $ ftyp_bod arg
       otherwise -> do
-        envLog (Error src (Ref "Function") ftyp (App fun arg) dep)
+        envLog (Error src (Ref "function") ftyp (App fun arg) dep)
         envFail
 
   go src (Ann chk val typ) dep = do
@@ -69,7 +69,7 @@ infer src term dep = debug ("infer: " ++ termShower False term dep) $ go src ter
     case M.lookup nam book of
       Just val -> infer src val dep
       Nothing  -> do
-        envLog (Error src (Ref "Term") (Ref "undefined") (Ref nam) dep)
+        envLog (Error src (Ref "expression") (Ref "undefined") (Ref nam) dep)
         envFail
 
   go src Set dep = do
@@ -369,4 +369,4 @@ doCheckRef nam = do
   book <- envGetBook
   case M.lookup nam book of
     Just val -> doCheck val
-    Nothing  -> envLog (Error Nothing (Ref "Term") (Ref "undefined") (Ref nam) 0) >> envFail
+    Nothing  -> envLog (Error Nothing (Ref "expression") (Ref "undefined") (Ref nam) 0) >> envFail

src/Kind/Show.hs

@@ -180,9 +180,9 @@ infoShow book fill info = case info of
         ctx' = contextShow book fill ctx dep
     in return $ concat ["\x1b[1mGOAL\x1b[0m ", nam', " : ", typ', "\n", ctx']
   Error src exp det bad dep -> do
-    let exp' = concat ["- expected: \x1b[32m", termShower True exp dep, "\x1b[0m"]
-        det' = concat ["- detected: \x1b[31m", termShower True det dep, "\x1b[0m"]
-        bad' = concat ["- bad_term: \x1b[2m", termShower True bad dep, "\x1b[0m"]
+    let exp' = concat ["- expected : \x1b[32m", termShower True exp dep, "\x1b[0m"]
+        det' = concat ["- detected : \x1b[31m", termShower True det dep, "\x1b[0m"]
+        bad' = concat ["- origin   : \x1b[2m", termShower True bad dep, "\x1b[0m"]
     (file, text) <- case src of
       Just (Cod (Loc fileName iniLine iniCol) (Loc _ endLine endCol)) -> do
         canonPath <- resolveToAbsolutePath fileName