@@ -316,11 +316,13 @@ elabCaseFun ind paramPos n ty cons info = do
316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
316 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
317 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
318 elimLog $ "-- case function definition: " ++ (show . showDeclImp verbosePPOption) eliminatorDef
318 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)
320 -- Do not elaborate clauses if there aren't any
321 -- Do not elaborate clauses if there aren't any
321 case eliminatorClauses of
322 case eliminatorClauses of
322 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
323 [] -> 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)
324 where elimLog :: String -> EliminatorState ()
326 where elimLog :: String -> EliminatorState ()
325 elimLog s = State.lift (logLvl 2 s)
327 elimLog s = State.lift (logLvl 2 s)