From ef9976ccdaa7c19fe1208cf64b1f43b3c0811d1b Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Mon, 30 May 2022 13:28:42 +0200
Subject: [PATCH] fix: do not discard macro exceptions in `expandMacro?`

---
 src/Lean/Elab/Util.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index 01de1dad2c..5dac434519 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -153,8 +153,8 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
     -- TODO: record recursive expansions in info tree?
     expandMacro?     := fun stx => do
       match (← expandMacroImpl? env stx) with
-      | some (_, Except.ok stx) => return some stx
-      | _                       => return none
+      | some (_, stx?) => liftExcept stx?
+      | none           => return none
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
     resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n