@@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do
316316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
317317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
318318 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
319− State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl) (\err -> return ())
319+ State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
320+ (ierror . Elaborating "type declaration of " elimDeclName)
320321 -- Do not elaborate clauses if there aren't any
321322 case eliminatorClauses of
322323 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
323− _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef) (\err -> return ())
324+ _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
325+ (ierror . Elaborating "clauses of " elimDeclName)
324326 where elimLog :: String -> EliminatorState ()
325327 elimLog s = State.lift (logLvl 2 s)
326328