diff --git a/nix/bootstrap.nix b/nix/bootstrap.nix
index 5ff0365148..21a6b2a71b 100644
--- a/nix/bootstrap.nix
+++ b/nix/bootstrap.nix
@@ -73,7 +73,7 @@ rec {
         src = ../src;
         fullSrc = ../.;
         inherit debug;
-        leanFlags = [ "-Dinterpreter.prefer_native=false" ];
+        leanFlags = [ "-Dinterpreter.prefer_native=true" ];
       });
     in (all: all // all.lean) rec {
       Init = build { name = "Init"; deps = []; };
diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index e49640f52a..fcb2ddb291 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -1877,14 +1877,18 @@ def reservedMacroScope := 0
 def firstFrontendMacroScope := hAdd reservedMacroScope 1
 
 class MonadRef (m : Type → Type) where
-  getRef      : m Syntax
-  withRef {α} : Syntax → m α → m α
+  getRef             : m Syntax
+  withRef {α}        : Syntax → m α → m α
+  getElaborator      : m Name
+  withElaborator {α} : Name → m α → m α
 
 export MonadRef (getRef)
 
 instance (m n : Type → Type) [MonadLift m n] [MonadFunctor m n] [MonadRef m] : MonadRef n where
-  getRef        := liftM (getRef : m _)
-  withRef ref x := monadMap (m := m) (MonadRef.withRef ref) x
+  getRef              := liftM (getRef : m _)
+  withRef ref x       := monadMap (m := m) (MonadRef.withRef ref) x
+  getElaborator       := liftM (MonadRef.getElaborator : m _)
+  withElaborator e x  := monadMap (m := m) (MonadRef.withElaborator e) x
 
 def replaceRef (ref : Syntax) (oldRef : Syntax) : Syntax :=
   match ref.getPos? with
@@ -2072,6 +2076,7 @@ structure Context where
   currRecDepth   : Nat := 0
   maxRecDepth    : Nat := defaultMaxRecDepth
   ref            : Syntax
+  elaborator     : Name
 
 inductive Exception where
   | error             : Syntax → String → Exception
@@ -2091,8 +2096,10 @@ abbrev Macro := Syntax → MacroM Syntax
 namespace Macro
 
 instance : MonadRef MacroM where
-  getRef     := bind read fun ctx => pure ctx.ref
-  withRef    := fun ref x => withReader (fun ctx => { ctx with ref := ref }) x
+  getRef           := bind read fun ctx => pure ctx.ref
+  withRef ref      := withReader (fun ctx => { ctx with ref })
+  getElaborator    := bind read fun ctx => pure ctx.elaborator
+  withElaborator e := withReader (fun ctx => { ctx with elaborator := e })
 
 def addMacroScope (n : Name) : MacroM Name :=
   bind read fun ctx =>
@@ -2184,6 +2191,8 @@ abbrev Unexpander := Syntax → UnexpandM Syntax
 instance : MonadQuotation UnexpandM where
   getRef              := pure Syntax.missing
   withRef             := fun _ => id
+  getElaborator       := pure Name.anonymous
+  withElaborator      := fun _ => id
   getCurrMacroScope   := pure 0
   getMainModule       := pure `_fakeMod
   withFreshMacroScope := id
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index 9af0a13f9b..582927208a 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -36,6 +36,7 @@ structure Context where
   currRecDepth   : Nat := 0
   maxRecDepth    : Nat := 1000
   ref            : Syntax := Syntax.missing
+  elaborator     : Name := Name.anonymous
   currNamespace  : Name := Name.anonymous
   openDecls      : List OpenDecl := []
   initHeartbeats : Nat := 0
@@ -53,6 +54,8 @@ instance : Inhabited (CoreM α) where
 instance : MonadRef CoreM where
   getRef := return (← read).ref
   withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
+  getElaborator := return (← read).elaborator
+  withElaborator e := withReader ({ · with elaborator := e })
 
 instance : MonadEnv CoreM where
   getEnv := return (← get).env
diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index acd4379051..555885d2d8 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -145,8 +145,7 @@ private def registerFailedToInferBinderTypeInfo (type : Expr) (ref : Syntax) : T
   registerCustomErrorIfMVar type ref "failed to infer binder type"
 
 private def addLocalVarInfoCore (lctx : LocalContext) (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
-  if (← getInfoState).enabled then
-    pushInfoTree <| InfoTree.node (children := {}) <| Info.ofTermInfo { lctx := lctx, expr := fvar, stx, expectedType? := none }
+  withLCtx lctx {} <| addTermInfo stx fvar
 
 private def addLocalVarInfo (stx : Syntax) (fvar : Expr) : TermElabM Unit := do
   addLocalVarInfoCore (← getLCtx) stx fvar
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 6a67225a10..29871d9124 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -49,6 +49,7 @@ structure Context where
   macroStack     : MacroStack := []
   currMacroScope : MacroScope := firstFrontendMacroScope
   ref            : Syntax := Syntax.missing
+  elaborator     : Name := Name.anonymous
 
 abbrev CommandElabCoreM (ε) := ReaderT Context $ StateRefT State $ EIO ε
 abbrev CommandElabM := CommandElabCoreM Exception
@@ -92,8 +93,10 @@ instance : AddMessageContext CommandElabM where
   addMessageContext := addMessageContextPartial
 
 instance : MonadRef CommandElabM where
-  getRef := Command.getRef
-  withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
+  getRef           := Command.getRef
+  withRef ref x    := withReader (fun ctx => { ctx with ref := ref }) x
+  getElaborator    := return (← read).elaborator
+  withElaborator e := withReader ({ · with elaborator := e })
 
 instance : MonadTrace CommandElabM where
   getTraceState := return (← get).traceState
@@ -207,12 +210,25 @@ private def addTraceAsMessages : CommandElabM Unit := do
     traceState.traces := {}
   }
 
-private def elabCommandUsing (s : State) (stx : Syntax) : List CommandElab → CommandElabM Unit
+private def elabCommandUsing (s : State) (stx : Syntax) : List (KeyedDeclsAttribute.AttributeEntry CommandElab) → CommandElabM Unit
   | []                => throwError "unexpected syntax{indentD stx}"
   | (elabFn::elabFns) =>
     catchInternalId unsupportedSyntaxExceptionId
-      (do elabFn stx; addTraceAsMessages)
+      (do
+        MonadRef.withElaborator elabFn.decl <| withInfoTreeContext (mkInfoTree := mkInfoTree) <| elabFn.value stx
+        addTraceAsMessages)
       (fun _ => do set s; addTraceAsMessages; elabCommandUsing s stx elabFns)
+where mkInfoTree trees := do
+  let ctx ← read
+  let s ← get
+  let scope := s.scopes.head!
+  let tree := InfoTree.node (Info.ofCommandInfo { elaborator := (← MonadRef.getElaborator), stx }) trees
+  let tree := InfoTree.context {
+    env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
+  } tree
+  if checkTraceOption (← getOptions) `Elab.info then
+    logTrace `Elab.info m!"{← tree.format}"
+  return tree
 
 /- Elaborate `x` with `stx` on the macro stack -/
 @[inline] def withMacroExpansion {α} (beforeStx afterStx : Syntax) (x : CommandElabM α) : CommandElabM α :=
@@ -248,19 +264,8 @@ register_builtin_option showPartialSyntaxErrors : Bool := {
 builtin_initialize registerTraceClass `Elab.command
 
 partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
-  let mkInfoTree trees := do
-    let ctx ← read
-    let s ← get
-    let scope := s.scopes.head!
-    let tree := InfoTree.node (Info.ofCommandInfo { stx := stx }) trees
-    let tree := InfoTree.context {
-      env := s.env, fileMap := ctx.fileMap, mctx := {}, currNamespace := scope.currNamespace, openDecls := scope.openDecls, options := scope.opts
-    } tree
-    if checkTraceOption (← getOptions) `Elab.info then
-      logTrace `Elab.info m!"{← tree.format}"
-    return tree
   let initMsgs ← modifyGet fun st => (st.messages, { st with messages := {} })
-  withLogging <| withRef stx <| withInfoTreeContext (mkInfoTree := mkInfoTree) <| withIncRecDepth <| withFreshMacroScope do
+  withLogging <| withRef stx <| withIncRecDepth <| withFreshMacroScope do
     runLinters stx
     match stx with
     | Syntax.node k args =>
@@ -271,13 +276,10 @@ partial def elabCommand (stx : Syntax) : CommandElabM Unit := do
       else do
         trace `Elab.command fun _ => stx;
         let s ← get
-        let stxNew? ← catchInternalId unsupportedSyntaxExceptionId
-          (do let newStx ← adaptMacro (getMacros s.env) stx; pure (some newStx))
-          (fun ex => pure none)
-        match stxNew? with
-        | some stxNew => withMacroExpansion stx stxNew <| elabCommand stxNew
+        match ← liftMacroM <| expandMacroImpl? s.env stx with
+        | some (decl, stxNew) => MonadRef.withElaborator decl <| withMacroExpansion stx stxNew <| elabCommand stxNew
         | _ =>
-          match commandElabAttribute.getValues s.env k with
+          match commandElabAttribute.getEntries s.env k with
           | []      => throwError "elaboration function for '{k}' has not been implemented"
           | elabFns => elabCommandUsing s stx elabFns
     | _ => throwError "unexpected command"
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 5932334a09..5acc9abafc 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -2,7 +2,7 @@
 Copyright (c) 2020 Wojciech Nawrocki. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 
-Authors: Wojciech Nawrocki, Leonardo de Moura
+Authors: Wojciech Nawrocki, Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Data.Position
 import Lean.Expr
@@ -27,15 +27,19 @@ structure ContextInfo where
   openDecls     : List OpenDecl  := []
   deriving Inhabited
 
-structure TermInfo where
+/-- An elaboration step -/
+structure ElabInfo where
+  elaborator : Name
+  stx : Syntax
+  deriving Inhabited
+
+structure TermInfo extends ElabInfo where
   lctx : LocalContext -- The local context when the term was elaborated.
   expectedType? : Option Expr
   expr : Expr
-  stx  : Syntax
   deriving Inhabited
 
-structure CommandInfo where
-  stx : Syntax
+structure CommandInfo extends ElabInfo where
   deriving Inhabited
 
 inductive CompletionInfo where
@@ -65,18 +69,16 @@ structure FieldInfo where
 /- We store the list of goals before and after the execution of a tactic.
    We also store the metavariable context at each time since, we want to unassigned metavariables
    at tactic execution time to be displayed as `?m...`. -/
-structure TacticInfo where
+structure TacticInfo extends ElabInfo where
   mctxBefore  : MetavarContext
   goalsBefore : List MVarId
-  stx         : Syntax
   mctxAfter   : MetavarContext
   goalsAfter  : List MVarId
   deriving Inhabited
 
-structure MacroExpansionInfo where
+structure MacroExpansionInfo extends ElabInfo where
   lctx   : LocalContext -- The local context when the macro was expanded.
-  before : Syntax
-  after  : Syntax
+  output : Syntax
   deriving Inhabited
 
 inductive Info where
@@ -189,9 +191,9 @@ def TacticInfo.format (ctx : ContextInfo) (info : TacticInfo) : IO Format := do
   return f!"Tactic @ {formatStxRange ctx info.stx}\n{info.stx}\nbefore {goalsBefore}\nafter {goalsAfter}"
 
 def MacroExpansionInfo.format (ctx : ContextInfo) (info : MacroExpansionInfo) : IO Format := do
-  let before ← ctx.ppSyntax info.lctx info.before
-  let after  ← ctx.ppSyntax info.lctx info.after
-  return f!"Macro expansion\n{before}\n===>\n{after}"
+  let stx    ← ctx.ppSyntax info.lctx info.stx
+  let output ← ctx.ppSyntax info.lctx info.output
+  return f!"Macro expansion\n{stx}\n===>\n{output}"
 
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
@@ -201,6 +203,14 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFieldInfo i          => i.format ctx
   | ofCompletionInfo i     => i.format ctx
 
+def Info.toElabInfo? : Info → Option ElabInfo
+  | ofTacticInfo i         => some i.toElabInfo
+  | ofTermInfo i           => some i.toElabInfo
+  | ofCommandInfo i        => some i.toElabInfo
+  | ofMacroExpansionInfo i => some i.toElabInfo
+  | ofFieldInfo i          => none
+  | ofCompletionInfo i     => none
+
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.
   We need this function because we preserve `TacticInfo` nodes during backtracking *and* their
@@ -259,14 +269,14 @@ def addCompletionInfo (info : CompletionInfo) : m Unit := do
 def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) (expectedType? : Option Expr := none) : m Name := do
   let n ← resolveGlobalConstNoOverload id
   if (← getInfoState).enabled then
-    pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
+    pushInfoLeaf <| Info.ofTermInfo { elaborator := (← MonadRef.getElaborator), lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
   return n
 
 def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) (expectedType? : Option Expr := none) : m (List Name) := do
   let ns ← resolveGlobalConst id
   if (← getInfoState).enabled then
     for n in ns do
-      pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
+      pushInfoLeaf <| Info.ofTermInfo { elaborator := (← MonadRef.getElaborator), lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx, expectedType? }
   return ns
 
 @[inline] def withInfoContext' [MonadFinally m] (x : m α) (mkInfo : α → m (Sum Info MVarId)) : m α := do
@@ -305,12 +315,12 @@ def assignInfoHoleId (mvarId : MVarId) (infoTree : InfoTree) : m Unit := do
   modifyInfoState fun s => { s with assignment := s.assignment.insert mvarId infoTree }
 end
 
-def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] (before after : Syntax) (x : m α) : m α :=
+def withMacroExpansionInfo [MonadFinally m] [Monad m] [MonadInfoTree m] [MonadLCtx m] [MonadRef m] (stx output : Syntax) (x : m α) : m α :=
   let mkInfo : m Info := do
     return Info.ofMacroExpansionInfo {
+      elaborator := ← MonadRef.getElaborator
       lctx   := (← getLCtx)
-      before := before
-      after  := after
+      stx, output
     }
   withInfoContext x mkInfo
 
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 50f64259a3..6478140622 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -13,6 +13,7 @@ namespace Lean.Elab.Level
 structure Context where
   options           : Options
   ref               : Syntax
+  elaborator        : Name
   autoBoundImplicit : Bool
 
 structure State where
@@ -26,8 +27,10 @@ instance : MonadOptions LevelElabM where
   getOptions := return (← read).options
 
 instance : MonadRef LevelElabM where
-  getRef        := return (← read).ref
-  withRef ref x := withReader (fun ctx => { ctx with ref := ref }) x
+  getRef           := return (← read).ref
+  withRef ref x    := withReader (fun ctx => { ctx with ref := ref }) x
+  getElaborator    := return (← read).elaborator
+  withElaborator e := withReader ({ · with elaborator := e })
 
 instance : AddMessageContext LevelElabM where
   addMessageContext msg := pure msg
diff --git a/src/Lean/Elab/Quotation/Precheck.lean b/src/Lean/Elab/Quotation/Precheck.lean
index 735252b431..24f59ebc6a 100644
--- a/src/Lean/Elab/Quotation/Precheck.lean
+++ b/src/Lean/Elab/Quotation/Precheck.lean
@@ -58,7 +58,7 @@ partial def precheck : Precheck := fun stx => do
     return
   if !hasQuotedIdent stx then
     return  -- we only precheck identifiers, so there is nothing to check here
-  if let some stx' ← liftMacroM <| Macro.expandMacro? stx then
+  if let some stx' ← liftMacroM <| expandMacro? stx then
     precheck stx'
     return
   throwErrorAt stx "no macro or `[quotPrecheck]` instance for syntax kind '{stx.getKind}' found{indentD stx}
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index 29d88dc984..6f47488d1f 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -109,33 +109,9 @@ unsafe def mkTacticAttribute : IO (KeyedDeclsAttribute Tactic) :=
 
 @[builtinInit mkTacticAttribute] constant tacticElabAttribute : KeyedDeclsAttribute Tactic
 
-/-
-Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
-the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
-and this is bad when rethrowing the exception at the `catch` block in these methods.
-We marked these places with a `(*)` in these methods.
--/
-
-private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List Tactic) : TacticM Unit := do
-  let rec loop : List Tactic → TacticM Unit
-    | []              => throwErrorAt stx "unexpected syntax {indentD stx}"
-    | evalFn::evalFns => do
-      try
-        evalFn stx
-      catch
-      | ex@(Exception.error _ _) =>
-        match evalFns with
-        | []      => throw ex -- (*)
-        | evalFns => s.restore; loop evalFns
-      | ex@(Exception.internal id _) =>
-        if id == unsupportedSyntaxExceptionId then
-          s.restore; loop evalFns
-        else
-          throw ex
-  loop tactics
-
 def mkTacticInfo (mctxBefore : MetavarContext) (goalsBefore : List MVarId) (stx : Syntax) : TacticM Info :=
   return Info.ofTacticInfo {
+    elaborator    := (← MonadRef.getElaborator)
     mctxBefore    := mctxBefore
     goalsBefore   := goalsBefore
     stx           := stx
@@ -151,23 +127,50 @@ def mkInitialTacticInfo (stx : Syntax) : TacticM (TacticM Info) := do
 @[inline] def withTacticInfoContext (stx : Syntax) (x : TacticM α) : TacticM α := do
   withInfoContext x (← mkInitialTacticInfo stx)
 
+/-
+Important: we must define `evalTacticUsing` and `expandTacticMacroFns` before we define
+the instance `MonadExcept` for `TacticM` since it backtracks the state including error messages,
+and this is bad when rethrowing the exception at the `catch` block in these methods.
+We marked these places with a `(*)` in these methods.
+-/
+
+private def evalTacticUsing (s : SavedState) (stx : Syntax) (tactics : List (KeyedDeclsAttribute.AttributeEntry Tactic)) : TacticM Unit := do
+  let rec loop
+    | []              => throwErrorAt stx "unexpected syntax {indentD stx}"
+    | evalFn::evalFns => do
+      try
+        MonadRef.withElaborator evalFn.decl <| withTacticInfoContext stx <| evalFn.value stx
+      catch
+      | ex@(Exception.error _ _) =>
+        match evalFns with
+        | []      => throw ex -- (*)
+        | evalFns => s.restore; loop evalFns
+      | ex@(Exception.internal id _) =>
+        if id == unsupportedSyntaxExceptionId then
+          s.restore; loop evalFns
+        else
+          throw ex
+  loop tactics
+
 mutual
 
-  partial def expandTacticMacroFns (stx : Syntax) (macros : List Macro) : TacticM Unit :=
-    let rec loop : List Macro → TacticM Unit
+  partial def expandTacticMacroFns (stx : Syntax) (macros : List (KeyedDeclsAttribute.AttributeEntry Macro)) : TacticM Unit :=
+    let rec loop
       | []    => throwErrorAt stx "tactic '{stx.getKind}' has not been implemented"
       | m::ms => do
         let scp ← getCurrMacroScope
         try
-          let stx' ← adaptMacro m stx
-          evalTactic stx'
+          MonadRef.withElaborator m.decl do
+            withTacticInfoContext stx do
+              let stx' ← adaptMacro m.value stx
+              evalTactic stx'
         catch ex =>
           if ms.isEmpty then throw ex -- (*)
           loop ms
     loop macros
 
   partial def expandTacticMacro (stx : Syntax) : TacticM Unit := do
-    expandTacticMacroFns stx (macroAttribute.getValues (← getEnv) stx.getKind)
+    expandTacticMacroFns stx (macroAttribute.getEntries (← getEnv) stx.getKind)
 
   partial def evalTacticAux (stx : Syntax) : TacticM Unit :=
     withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
@@ -178,13 +181,13 @@ mutual
         else do
           trace[Elab.step] "{stx}"
           let s ← Tactic.saveState
-          match tacticElabAttribute.getValues (← getEnv) stx.getKind with
+          match tacticElabAttribute.getEntries (← getEnv) stx.getKind with
           | []      => expandTacticMacro stx
           | evalFns => evalTacticUsing s stx evalFns
       | _ => throwError m!"unexpected tactic{indentD stx}"
 
   partial def evalTactic (stx : Syntax) : TacticM Unit :=
-    withTacticInfoContext stx (evalTacticAux stx)
+    evalTacticAux stx
 
 end
 
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index b42745306a..b678530e8f 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Leonardo de Moura
+Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.ResolveName
 import Lean.Util.Sorry
@@ -390,10 +390,9 @@ open Level (LevelElabM)
 
 def liftLevelM (x : LevelElabM α) : TermElabM α := do
   let ctx ← read
-  let ref ← getRef
   let mctx ← getMCtx
   let ngen ← getNGen
-  let lvlCtx : Level.Context := { options := (← getOptions), ref := ref, autoBoundImplicit := ctx.autoBoundImplicit }
+  let lvlCtx : Level.Context := { options := (← getOptions), ref := (← getRef), elaborator := (← MonadRef.getElaborator), autoBoundImplicit := ctx.autoBoundImplicit }
   match (x lvlCtx).run { ngen := ngen, mctx := mctx, levelNames := (← getLevelNames) } with
   | EStateM.Result.ok a newS  => setMCtx newS.mctx; setNGen newS.ngen; setLevelNames newS.levelNames; pure a
   | EStateM.Result.error ex _ => throw ex
@@ -933,51 +932,80 @@ private def postponeElabTerm (stx : Syntax) (expectedType? : Option Expr) : Term
   registerSyntheticMVar stx mvar.mvarId! (SyntheticMVarKind.postponed (← saveContext))
   pure mvar
 
+def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
+  return (← get).syntheticMVars.find? fun d => d.mvarId == mvarId
+
+def mkTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM (Sum Info MVarId) := do
+  let isHole? : TermElabM (Option MVarId) := do
+    match e with
+    | Expr.mvar mvarId _ =>
+      match (← getSyntheticMVarDecl? mvarId) with
+      | some { kind := SyntheticMVarKind.tactic .., .. }    => return mvarId
+      | some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId
+      | _                                                   => return none
+    | _ => pure none
+  match (← isHole?) with
+  | none        => return Sum.inl <| Info.ofTermInfo { elaborator := (← MonadRef.getElaborator), lctx := (← getLCtx), expr := e, stx, expectedType? }
+  | some mvarId => return Sum.inr mvarId
+
+def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM Unit := do
+  withInfoContext' (pure ()) (fun _ => mkTermInfo stx e expectedType?) |> discard
+
 /-
   Helper function for `elabTerm` is tries the registered elaboration functions for `stxNode` kind until it finds one that supports the syntax or
   an error is found. -/
 private def elabUsingElabFnsAux (s : SavedState) (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool)
-    : List TermElab → TermElabM Expr
+    : List (KeyedDeclsAttribute.AttributeEntry TermElab) → TermElabM Expr
   | []                => do throwError "unexpected syntax{indentD stx}"
-  | (elabFn::elabFns) => do
+  | (elabFn::elabFns) =>
     try
-      elabFn stx expectedType?
+      -- record elaborator in info tree, but only when not backtracking to other elaborators (outer `try`)
+      MonadRef.withElaborator elabFn.decl <| withInfoContext' (mkInfo := mkTermInfo (expectedType? := expectedType?) stx)
+        (try
+          elabFn.value stx expectedType?
+        catch ex => match ex with
+          | Exception.error ref msg =>
+            if (← read).errToSorry then
+              exceptionToSorry ex expectedType?
+            else
+              throw ex
+          | Exception.internal id _ =>
+            if (← read).errToSorry && id == abortTermExceptionId then
+              exceptionToSorry ex expectedType?
+            else if id == unsupportedSyntaxExceptionId then
+              throw ex  -- to outer try
+            else if catchExPostpone && id == postponeExceptionId then
+              /- If `elab` threw `Exception.postpone`, we reset any state modifications.
+                For example, we want to make sure pending synthetic metavariables created by `elab` before
+                it threw `Exception.postpone` are discarded.
+                Note that we are also discarding the messages created by `elab`.
+
+                For example, consider the expression.
+                `((f.x a1).x a2).x a3`
+                Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
+                Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
+                because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
+                finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
+                keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
+                wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
+                and new metavariables are created for the nested functions. -/
+              s.restore
+              postponeElabTerm stx expectedType?
+            else
+              throw ex)
     catch ex => match ex with
-      | Exception.error ref msg =>
-        if (← read).errToSorry then
-          exceptionToSorry ex expectedType?
+      | Exception.internal id _ =>
+        if id == unsupportedSyntaxExceptionId then
+          s.restore  -- also removes the info tree created above
+          elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
         else
           throw ex
-      | Exception.internal id _ =>
-        if (← read).errToSorry && id == abortTermExceptionId then
-          exceptionToSorry ex expectedType?
-        else if id == unsupportedSyntaxExceptionId then
-          s.restore
-          elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
-        else if catchExPostpone && id == postponeExceptionId then
-          /- If `elab` threw `Exception.postpone`, we reset any state modifications.
-             For example, we want to make sure pending synthetic metavariables created by `elab` before
-             it threw `Exception.postpone` are discarded.
-             Note that we are also discarding the messages created by `elab`.
-
-             For example, consider the expression.
-             `((f.x a1).x a2).x a3`
-             Now, suppose the elaboration of `f.x a1` produces an `Exception.postpone`.
-             Then, a new metavariable `?m` is created. Then, `?m.x a2` also throws `Exception.postpone`
-             because the type of `?m` is not yet known. Then another, metavariable `?n` is created, and
-            finally `?n.x a3` also throws `Exception.postpone`. If we did not restore the state, we would
-            keep "dead" metavariables `?m` and `?n` on the pending synthetic metavariable list. This is
-            wasteful because when we resume the elaboration of `((f.x a1).x a2).x a3`, we start it from scratch
-            and new metavariables are created for the nested functions. -/
-            s.restore
-            postponeElabTerm stx expectedType?
-          else
-            throw ex
+      | _ => throw ex
 
 private def elabUsingElabFns (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone : Bool) : TermElabM Expr := do
   let s ← saveState
   let k := stx.getKind
-  match termElabAttribute.getValues (← getEnv) k with
+  match termElabAttribute.getEntries (← getEnv) k with
   | []      => throwError "elaboration function for '{k}' has not been implemented{indentD stx}"
   | elabFns => elabUsingElabFnsAux s stx expectedType? catchExPostpone elabFns
 
@@ -1107,40 +1135,21 @@ private partial def elabTermAux (expectedType? : Option Expr) (catchExPostpone :
     checkMaxHeartbeats "elaborator"
     withNestedTraces do
     let env ← getEnv
-    let stxNew? ← catchInternalId unsupportedSyntaxExceptionId
-      (do let newStx ← adaptMacro (getMacros env) stx; pure (some newStx))
-      (fun _ => pure none)
-    match stxNew? with
-    | some stxNew => withMacroExpansion stx stxNew <| withRef stxNew <| elabTermAux expectedType? catchExPostpone implicitLambda stxNew
+    match ← liftMacroM (expandMacroImpl? env stx) with
+    | some (decl, stxNew) =>
+      MonadRef.withElaborator decl <|
+        withMacroExpansion stx stxNew <|
+          withRef stxNew <|
+            elabTermAux expectedType? catchExPostpone implicitLambda stxNew
     | _ =>
       let implicit? ← if implicitLambda && (← read).implicitLambda then useImplicitLambda? stx expectedType? else pure none
       match implicit? with
       | some expectedType => elabImplicitLambda stx catchExPostpone expectedType
       | none              => elabUsingElabFns stx expectedType? catchExPostpone
 
-def addTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM Unit := do
-  if (← getInfoState).enabled then
-    pushInfoLeaf <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx, expectedType? }
-
-def getSyntheticMVarDecl? (mvarId : MVarId) : TermElabM (Option SyntheticMVarDecl) :=
-  return (← get).syntheticMVars.find? fun d => d.mvarId == mvarId
-
-def mkTermInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr := none) : TermElabM (Sum Info MVarId) := do
-  let isHole? : TermElabM (Option MVarId) := do
-    match e with
-    | Expr.mvar mvarId _ =>
-      match (← getSyntheticMVarDecl? mvarId) with
-      | some { kind := SyntheticMVarKind.tactic .., .. }    => return mvarId
-      | some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId
-      | _                                                   => return none
-    | _ => pure none
-  match (← isHole?) with
-  | none        => return Sum.inl <| Info.ofTermInfo { lctx := (← getLCtx), expr := e, stx, expectedType? }
-  | some mvarId => return Sum.inr mvarId
-
 /-- Store in the `InfoTree` that `e` is a "dot"-completion target. -/
 def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr) (field? : Option Syntax := none) : TermElabM Unit := do
-  addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), expectedType? } (field? := field?) (expectedType? := expectedType?)
+  addCompletionInfo <| CompletionInfo.dot { expr := e, stx, lctx := (← getLCtx), elaborator := (← MonadRef.getElaborator), expectedType? } (field? := field?) (expectedType? := expectedType?)
 
 /--
   Main function for elaborating terms.
@@ -1160,7 +1169,7 @@ def addDotCompletionInfo (stx : Syntax) (e : Expr) (expectedType? : Option Expr)
   We use this flag to implement, for example, the `@` modifier. If `Context.implicitLambda == false`, then this parameter has no effect.
   -/
 def elabTerm (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) : TermElabM Expr :=
-  withInfoContext' (withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx) (mkTermInfo stx (expectedType? := expectedType?))
+  withRef stx <| elabTermAux expectedType? catchExPostpone implicitLambda stx
 
 def elabTermEnsuringType (stx : Syntax) (expectedType? : Option Expr) (catchExPostpone := true) (implicitLambda := true) (errorMsgHeader? : Option String := none) : TermElabM Expr := do
   let e ← elabTerm stx expectedType? catchExPostpone implicitLambda
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index c1c6cd52ee..b7c1cc8846 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -119,17 +119,15 @@ constant mkMacroAttribute : IO (KeyedDeclsAttribute Macro)
 
 builtin_initialize macroAttribute : KeyedDeclsAttribute Macro ← mkMacroAttribute
 
-private def expandMacroFns (stx : Syntax) : List Macro → MacroM Syntax
-  | []    => throw Macro.Exception.unsupportedSyntax
-  | m::ms => do
+def expandMacroImpl? (env : Environment) : Syntax → MacroM (Option (Name × Syntax)) := fun stx => do
+  for e in macroAttribute.getEntries env stx.getKind do
     try
-      m stx
+      let stx' ← e.value stx
+      return (e.decl, stx')
     catch
-      | Macro.Exception.unsupportedSyntax => expandMacroFns stx ms
+      | Macro.Exception.unsupportedSyntax => pure ()
       | ex                                => throw ex
-
-def getMacros (env : Environment) : Macro := fun stx =>
-  expandMacroFns stx (macroAttribute.getValues env stx.getKind)
+  return none
 
 class MonadMacroAdapter (m : Type → Type) where
   getCurrMacroScope                  : m MacroScope
@@ -142,20 +140,16 @@ instance (m n) [MonadLift m n] [MonadMacroAdapter m] : MonadMacroAdapter n := {
   setNextMacroScope := fun s => liftM (MonadMacroAdapter.setNextMacroScope s : m _)
 }
 
-private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syntax) := do
-  try
-    let newStx ← getMacros env stx
-    pure (some newStx)
-  catch
-    | Macro.Exception.unsupportedSyntax => pure none
-    | ex                                => throw ex
-
 def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] [MonadTrace m] [MonadOptions m] [AddMessageContext m] (x : MacroM α) : m α := do
   let env  ← getEnv
   let currNamespace ← getCurrNamespace
   let openDecls ← getOpenDecls
   let methods := Macro.mkMethods {
-    expandMacro?     := expandMacro? env
+    -- TODO: record recursive expansions in info tree?
+    expandMacro?     := fun stx => do
+      match ← expandMacroImpl? env stx with
+      | some (_, stx) => some stx
+      | none          => none
     hasDecl          := fun declName => return env.contains declName
     getCurrNamespace := return currNamespace
     resolveNamespace? := fun n => return ResolveName.resolveNamespace? env currNamespace openDecls n
@@ -163,6 +157,7 @@ def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEn
   }
   match x { methods        := methods
             ref            := ← getRef
+            elaborator     := ← MonadRef.getElaborator
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope
             mainModule     := env.mainModule
             currRecDepth   := ← MonadRecDepth.getRecDepth
diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean
index 97c2d835a4..b73a5d6dcc 100644
--- a/src/Lean/Hygiene.lean
+++ b/src/Lean/Hygiene.lean
@@ -29,15 +29,17 @@ structure Unhygienic.Context where
     corresponding to `withFreshMacroScope` calls. -/
 abbrev Unhygienic := ReaderT Lean.Unhygienic.Context $ StateM MacroScope
 namespace Unhygienic
-instance : MonadQuotation Unhygienic := {
-  getRef              := do (← read).ref,
-  withRef             := fun ref => withReader ({ · with ref := ref }),
-  getCurrMacroScope   := do (← read).scope,
-  getMainModule       := pure `UnhygienicMain,
+instance : MonadQuotation Unhygienic where
+  getRef              := do (← read).ref
+  withRef             := fun ref => withReader ({ · with ref := ref })
+  getElaborator       := pure Name.anonymous
+  withElaborator      := fun _ => id
+  getCurrMacroScope   := do (← read).scope
+  getMainModule       := pure `UnhygienicMain
   withFreshMacroScope := fun x => do
     let fresh ← modifyGet fun n => (n, n + 1)
     withReader ({ · with scope := fresh}) x
-}
+
 protected def run {α : Type} (x : Unhygienic α) : α := (x ⟨Syntax.missing, firstFrontendMacroScope⟩).run' (firstFrontendMacroScope+1)
 end Unhygienic
 
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 632b74fb05..4d1c108bc2 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -57,7 +57,7 @@ def Info.stx : Info → Syntax
   | ofTacticInfo i         => i.stx
   | ofTermInfo i           => i.stx
   | ofCommandInfo i        => i.stx
-  | ofMacroExpansionInfo i => i.before
+  | ofMacroExpansionInfo i => i.stx
   | ofFieldInfo i          => i.stx
   | ofCompletionInfo i     => i.stx
 
diff --git a/src/stdlib.make.in b/src/stdlib.make.in
index 2d87c4acd9..fed8bfd40d 100644
--- a/src/stdlib.make.in
+++ b/src/stdlib.make.in
@@ -14,7 +14,7 @@ LEANMAKE_OPTS=\
 	LIB_OUT="${LIB}/lean"\
 	OLEAN_OUT="${LIB}/lean"\
 	BIN_OUT="${CMAKE_BINARY_DIR}/bin"\
-	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=false"\
+	LEAN_OPTS+="${LEAN_EXTRA_MAKE_OPTS} -Dinterpreter.prefer_native=true"\
 	LEANC_OPTS+="${LEANC_OPTS}"\
 	LEAN_CXX="${CMAKE_CXX_COMPILER_LAUNCHER} ${CMAKE_CXX_COMPILER}"\
 	LEAN_AR="${CMAKE_AR}"\
diff --git a/tests/lean/infoTree.lean.expected.out b/tests/lean/infoTree.lean.expected.out
index e6394dabcb..b86d95fcbd 100644
--- a/tests/lean/infoTree.lean.expected.out
+++ b/tests/lean/infoTree.lean.expected.out
@@ -3,11 +3,11 @@
     [.] `Nat : some Sort.{?_uniq.535} @ ⟨13, 11⟩-⟨13, 14⟩
     Nat : Type @ ⟨13, 11⟩-⟨13, 14⟩
   x : Nat @ ⟨13, 7⟩-⟨13, 8⟩
-  Nat × Nat : Type @ ⟨13, 18⟩-⟨13, 27⟩
-    Macro expansion
-    Nat × Nat
-    ===>
-    Prod✝ Nat Nat
+  Macro expansion
+  Nat × Nat
+  ===>
+  Prod✝ Nat Nat
+    Nat × Nat : Type @ ⟨13, 18⟩†-⟨13, 27⟩
       Prod : Type → Type → Type @ ⟨13, 18⟩†-⟨13, 22⟩†
       Nat : Type @ ⟨13, 18⟩-⟨13, 21⟩
         [.] `Nat : some Type.{?_uniq.539} @ ⟨13, 18⟩-⟨13, 21⟩
@@ -50,16 +50,16 @@
         [.] `Bool : some Sort.{?_uniq.573} @ ⟨17, 27⟩-⟨17, 31⟩
         Bool : Type @ ⟨17, 27⟩-⟨17, 31⟩
       b : Bool @ ⟨17, 23⟩-⟨17, 24⟩
-      x + 0 = x : Prop @ ⟨17, 35⟩-⟨17, 44⟩
-        Macro expansion
-        x + 0 = x
-        ===>
-        binrel% Eq✝ (x + 0)x
-          x + 0 : Nat @ ⟨17, 35⟩-⟨17, 40⟩
-            Macro expansion
-            x + 0
-            ===>
-            binop% HAdd.hAdd✝ x 0
+      Macro expansion
+      x + 0 = x
+      ===>
+      binrel% Eq✝ (x + 0)x
+        x + 0 = x : Prop @ ⟨17, 35⟩†-⟨17, 44⟩
+          Macro expansion
+          x + 0
+          ===>
+          binop% HAdd.hAdd✝ x 0
+            x + 0 : Nat @ ⟨17, 35⟩†-⟨17, 40⟩
               Macro expansion
               binop% HAdd.hAdd✝ x 0
               ===>
@@ -160,26 +160,26 @@
           let z1 : Nat := z + w;
           z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
           Nat × Nat : Type @ ⟨23, 4⟩-⟨23, 7⟩
-          (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩-⟨23, 32⟩
-            Macro expansion
-            (x + y, x - y)
-            ===>
-            Prod.mk✝ (x + y) (x - y)
+          Macro expansion
+          (x + y, x - y)
+          ===>
+          Prod.mk✝ (x + y) (x - y)
+            (x + y, x - y) : Nat × Nat @ ⟨23, 18⟩†-⟨23, 31⟩
               Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 18⟩†-⟨23, 25⟩†
-              x + y : Nat @ ⟨23, 19⟩-⟨23, 24⟩
-                Macro expansion
-                x + y
-                ===>
-                binop% HAdd.hAdd✝ x y
+              Macro expansion
+              x + y
+              ===>
+              binop% HAdd.hAdd✝ x y
+                x + y : Nat @ ⟨23, 19⟩†-⟨23, 24⟩
                   x : Nat @ ⟨23, 19⟩-⟨23, 20⟩
                     x : Nat @ ⟨23, 19⟩-⟨23, 20⟩
                   y : Nat @ ⟨23, 23⟩-⟨23, 24⟩
                     y : Nat @ ⟨23, 23⟩-⟨23, 24⟩
-              x - y : Nat @ ⟨23, 26⟩-⟨23, 31⟩
-                Macro expansion
-                x - y
-                ===>
-                binop% HSub.hSub✝ x y
+              Macro expansion
+              x - y
+              ===>
+              binop% HSub.hSub✝ x y
+                x - y : Nat @ ⟨23, 26⟩†-⟨23, 31⟩
                   x : Nat @ ⟨23, 26⟩-⟨23, 27⟩
                     x : Nat @ ⟨23, 26⟩-⟨23, 27⟩
                   y : Nat @ ⟨23, 30⟩-⟨23, 31⟩
@@ -189,45 +189,49 @@
           | (z, w) =>
             let z1 : Nat := z + w;
             z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
-            Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
-            [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
-            [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
-            (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
-              Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨23, 11⟩†
-              Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
-              Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
-              z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
+            match x✝ with 
+            | (z, w) =>
+              let z1 : Nat := z + w;
+              z + z1 : Nat @ ⟨23, 4⟩†-⟨25, 10⟩
+              Prod.mk : {α : Type ?u} → {β : Type ?u} → α → β → α × β @ ⟨23, 4⟩†-⟨25, 10⟩†
+              [.] `z : none @ ⟨23, 9⟩-⟨23, 10⟩
+              [.] `w : none @ ⟨23, 12⟩-⟨23, 13⟩
+              (z, w) : Nat × Nat @ ⟨23, 4⟩†-⟨23, 13⟩
+                Prod.mk : {α β : Type} → α → β → α × β @ ⟨23, 4⟩†-⟨23, 11⟩†
+                Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
+                Nat : Type @ ⟨23, 4⟩†-⟨23, 13⟩†
                 z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
-              w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
+                  z : Nat @ ⟨23, 9⟩-⟨23, 10⟩
                 w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
-            let z1 : Nat := z + w;
-            z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩
-              Nat : Type @ ⟨24, 8⟩-⟨24, 10⟩
-              z + w : Nat @ ⟨24, 14⟩-⟨24, 19⟩
+                  w : Nat @ ⟨23, 12⟩-⟨23, 13⟩
+              let z1 : Nat := z + w;
+              z + z1 : Nat @ ⟨24, 4⟩-⟨25, 10⟩
+                Nat : Type @ ⟨24, 8⟩-⟨24, 10⟩
                 Macro expansion
                 z + w
                 ===>
                 binop% HAdd.hAdd✝ z w
-                  z : Nat @ ⟨24, 14⟩-⟨24, 15⟩
+                  z + w : Nat @ ⟨24, 14⟩†-⟨24, 19⟩
                     z : Nat @ ⟨24, 14⟩-⟨24, 15⟩
-                  w : Nat @ ⟨24, 18⟩-⟨24, 19⟩
+                      z : Nat @ ⟨24, 14⟩-⟨24, 15⟩
                     w : Nat @ ⟨24, 18⟩-⟨24, 19⟩
-              z1 : Nat @ ⟨24, 8⟩-⟨24, 10⟩
-              z + z1 : Nat @ ⟨25, 4⟩-⟨25, 10⟩
+                      w : Nat @ ⟨24, 18⟩-⟨24, 19⟩
+                z1 : Nat @ ⟨24, 8⟩-⟨24, 10⟩
                 Macro expansion
                 z + z1
                 ===>
                 binop% HAdd.hAdd✝ z z1
-                  z : Nat @ ⟨25, 4⟩-⟨25, 5⟩
+                  z + z1 : Nat @ ⟨25, 4⟩†-⟨25, 10⟩
                     z : Nat @ ⟨25, 4⟩-⟨25, 5⟩
-                  z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩
+                      z : Nat @ ⟨25, 4⟩-⟨25, 5⟩
                     z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩
+                      z1 : Nat @ ⟨25, 8⟩-⟨25, 10⟩
 [Elab.info] command @ ⟨27, 0⟩-⟨28, 17⟩
-  Nat × Array (Array Nat) : Type @ ⟨27, 12⟩-⟨27, 35⟩
-    Macro expansion
-    Nat × Array (Array Nat)
-    ===>
-    Prod✝ Nat (Array (Array Nat))
+  Macro expansion
+  Nat × Array (Array Nat)
+  ===>
+  Prod✝ Nat (Array (Array Nat))
+    Nat × Array (Array Nat) : Type @ ⟨27, 12⟩†-⟨27, 35⟩
       Prod : Type → Type → Type @ ⟨27, 12⟩†-⟨27, 16⟩†
       Nat : Type @ ⟨27, 12⟩-⟨27, 15⟩
         [.] `Nat : some Type.{?_uniq.1900} @ ⟨27, 12⟩-⟨27, 15⟩
@@ -235,11 +239,11 @@
       Array (Array Nat) : Type @ ⟨27, 18⟩-⟨27, 35⟩
         [.] `Array : some Type.{?_uniq.1899} @ ⟨27, 18⟩-⟨27, 23⟩
         Array : Type → Type @ ⟨27, 18⟩-⟨27, 23⟩
-        Array Nat : Type @ ⟨27, 24⟩-⟨27, 35⟩
-          Macro expansion
-          (Array Nat)
-          ===>
-          Array Nat
+        Macro expansion
+        (Array Nat)
+        ===>
+        Array Nat
+          Array Nat : Type @ ⟨27, 25⟩-⟨27, 34⟩
             [.] `Array : some Type.{?_uniq.1901} @ ⟨27, 25⟩-⟨27, 30⟩
             Array : Type → Type @ ⟨27, 25⟩-⟨27, 30⟩
             Nat : Type @ ⟨27, 31⟩-⟨27, 34⟩
@@ -288,11 +292,11 @@
     [.] `B : some Sort.{?_uniq.1970} @ ⟨33, 19⟩-⟨33, 20⟩
     B : Type @ ⟨33, 19⟩-⟨33, 20⟩
   { pair := ({ val := id }, { val := id }) } : B @ ⟨33, 24⟩-⟨35, 1⟩
-    ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩-⟨34, 40⟩
-      Macro expansion
-      ({ val := id }, { val := id })
-      ===>
-      Prod.mk✝ { val := id } { val := id }
+    Macro expansion
+    ({ val := id }, { val := id })
+    ===>
+    Prod.mk✝ { val := id } { val := id }
+      ({ val := id }, { val := id }) : A × A @ ⟨34, 10⟩†-⟨34, 39⟩
         Prod.mk : {α β : Type} → α → β → α × β @ ⟨34, 10⟩†-⟨34, 17⟩†
         { val := id } : A @ ⟨34, 11⟩-⟨34, 24⟩
           id : Nat → Nat @ ⟨34, 20⟩-⟨34, 22⟩
diff --git a/tests/lean/interactive/plainTermGoal.lean.expected.out b/tests/lean/interactive/plainTermGoal.lean.expected.out
index 810a9271b9..8b75593022 100644
--- a/tests/lean/interactive/plainTermGoal.lean.expected.out
+++ b/tests/lean/interactive/plainTermGoal.lean.expected.out
@@ -16,7 +16,7 @@
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 29}}
 {"range":
- {"start": {"line": 2, "character": 28}, "end": {"line": 2, "character": 46}},
+ {"start": {"line": 2, "character": 29}, "end": {"line": 2, "character": 45}},
  "goal": "⊢ 1 < 2"}
 {"textDocument": {"uri": "file://plainTermGoal.lean"},
  "position": {"line": 2, "character": 44}}
diff --git a/tests/lean/run/methodsRetInhabited.lean b/tests/lean/run/methodsRetInhabited.lean
index 5df0496087..39f9985a99 100644
--- a/tests/lean/run/methodsRetInhabited.lean
+++ b/tests/lean/run/methodsRetInhabited.lean
@@ -2,6 +2,7 @@ open Lean
 
 def exec (x : MacroM α) : Option α :=
   match x {
+      elaborator := Name.anonymous
       mainModule := `Expander
       currMacroScope := 0
       ref := arbitrary