@@ -457,3 +457,21 @@ readFile fn = do h <- openFile fn Read
457 if not x then do l <- fread h
457 if not x then do l <- fread h
458 readFile' h (contents ++ l)
458 readFile' h (contents ++ l)
459 else return contents
459 else return contents
461+------- Some error rewriting
463+%language ErrorReflection
465+cast_part : TT -> ErrorReportPart
466+cast_part (P Bound n t) = TextPart "unknown type"
467+cast_part x = TermPart x
470+cast_error : Err -> Maybe (List ErrorReportPart)
471+cast_error (CantResolve `(Cast ~x ~y))
472+ = Just [TextPart "Can't cast from",
476+cast_error _ = Nothing