@@ -1632,6 +1632,8 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)
1632 then handle err
1632 then handle err
1633 else applyHandlers err hs
1633 else applyHandlers err hs
1634 return (ElaboratingArg f a prev err')
1634 return (ElaboratingArg f a prev err')
1635+ -- ProofSearchFail is an internal detail - so don't expose it
1636+ handle (ProofSearchFail e) = handle e
1635 -- TODO: argument-specific error handlers go here for ElaboratingArg
1637 -- TODO: argument-specific error handlers go here for ElaboratingArg
1636 handle e = do ist <- getIState
1638 handle e = do ist <- getIState
1637 logLvl 2 "Starting error reflection"
1639 logLvl 2 "Starting error reflection"