@@ -317,12 +317,12 @@ elabCaseFun ind paramPos n ty cons info = do
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)
319 State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorTyDecl)
320− (\err -> do { e <- showErr err ; logLvl 2 ("Error while elaborating eliminator type declaration: " ++ e)})
320+ (ierror . Elaborating "type declaration of " elimDeclName)
321 -- Do not elaborate clauses if there aren't any
321 -- Do not elaborate clauses if there aren't any
322 case eliminatorClauses of
322 case eliminatorClauses of
323 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
323 [] -> State.lift $ solveDeferred elimDeclName -- Remove meta-variable for type
324 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
324 _ -> State.lift $ idrisCatch (rec_elabDecl info EAll info eliminatorDef)
325− (\err -> do { e <- showErr err ; logLvl 2 ("Error while elaborating eliminator clauses: " ++ e)})
325+ (ierror . Elaborating "clauses of " elimDeclName)
326 where elimLog :: String -> EliminatorState ()
326 where elimLog :: String -> EliminatorState ()
327 elimLog s = State.lift (logLvl 2 s)
327 elimLog s = State.lift (logLvl 2 s)