From 5103040063e64c97dca5e46fc5120ea404ddd87d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 13 Aug 2020 09:14:46 -0700 Subject: [PATCH] chore: fix parameter --- src/Lean/Elab/Log.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean index 2c94a887f9..ea239341a2 100644 --- a/src/Lean/Elab/Log.lean +++ b/src/Lean/Elab/Log.lean @@ -66,10 +66,10 @@ log stx MessageSeverity.warning msgData def logInfo [MonadLog m] (stx : Syntax) (msgData : MessageData) : m Unit := log stx MessageSeverity.information msgData -def throwError {α} [MonadPosInfo m] [MonadExceptCore Exception m] (ref : Syntax) (msgData : MessageData) : m α := do +def throwError {α} [MonadPosInfo m] [MonadExcept Exception m] (ref : Syntax) (msgData : MessageData) : m α := do msg ← mkMessage msgData MessageSeverity.error ref; throw (Exception.error msg) -def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExceptCore Exception m] (msgData : MessageData) : m α := do +def throwErrorUsingCmdPos {α} [MonadPosInfo m] [MonadExcept Exception m] (msgData : MessageData) : m α := do cmdPos ← getCmdPos; msg ← mkMessageAt msgData MessageSeverity.error cmdPos; throw (Exception.error msg)