diff --git a/src/Lean/Elab/Declaration.lean b/src/Lean/Elab/Declaration.lean
index 3b111a6d2d..cfff571c32 100644
--- a/src/Lean/Elab/Declaration.lean
+++ b/src/Lean/Elab/Declaration.lean
@@ -271,7 +271,7 @@ def elabMutual : CommandElab := fun stx => do
   let attrs ← elabAttrs attrInsts
   let idents := stx[4].getArgs
   for ident in idents do withRef ident <| liftTermElabM none do
-    let declName ← resolveGlobalConstNoOverload ident.getId
+    let declName ← resolveGlobalConstNoOverloadWithInfo ident
     Term.applyAttributes declName attrs
     for attrName in toErase do
       Attribute.erase declName attrName
diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean
index 0d2ae2c4c1..734d77506d 100644
--- a/src/Lean/Elab/Deriving/Basic.lean
+++ b/src/Lean/Elab/Deriving/Basic.lean
@@ -32,8 +32,8 @@ def applyDerivingHandlers (className : Name) (typeNames : Array Name) : CommandE
 
 @[builtinCommandElab «deriving»] def elabDeriving : CommandElab
   | `(deriving instance $[$classes],* for $[$declNames],*) => do
-     let classes ← classes.mapM (resolveGlobalConstNoOverload ·.getId)
-     let declNames ← declNames.mapM (resolveGlobalConstNoOverload ·.getId)
+     let classes ← classes.mapM resolveGlobalConstNoOverloadWithInfo
+     let declNames ← declNames.mapM resolveGlobalConstNoOverloadWithInfo
      for cls in classes do
        try
          applyDerivingHandlers cls declNames
@@ -46,12 +46,12 @@ structure DerivingClassView where
   className : Name
 
 /- leading_parser optional (atomic ("deriving " >> notSymbol "instance") >> sepBy1 ident ", ") -/
-def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
+def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do
   if optDeriving.isNone then
     return #[]
   else
     optDeriving[0][1].getSepArgs.mapM fun ident => do
-      let className ← resolveGlobalConstNoOverload ident.getId
+      let className ← resolveGlobalConstNoOverloadWithInfo ident
       return { ref := ident, className := className }
 
 def DerivingClassView.applyHandlers (view : DerivingClassView) (declNames : Array Name) : CommandElabM Unit :=
diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index d638148659..8f02b9028f 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -191,11 +191,17 @@ def pushInfoLeaf (t : Info) : m Unit := do
   if (← getInfoState).enabled then
     pushInfoTree <| InfoTree.node (children := {}) t
 
-def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (id : Syntax) : m (List Name) := do
-  let ns ← resolveGlobalConst id.getId
+def resolveGlobalConstNoOverloadWithInfo [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) : m Name := do
+  let n ← resolveGlobalConstNoOverload id
+  if (← getInfoState).enabled then
+    pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := stx }
+  return n
+
+def resolveGlobalConstWithInfos [MonadResolveName m] [MonadEnv m] [MonadError m] (stx : Syntax) (id := stx.getId) : 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 := id }
+      pushInfoLeaf <| Info.ofTermInfo { lctx := LocalContext.empty, expr := (← mkConstWithLevelParams n), stx := stx }
   return ns
 
 def mkInfoNode (info : Info) : m Unit := do
diff --git a/src/Lean/Elab/Print.lean b/src/Lean/Elab/Print.lean
index d23007daf6..bead86786e 100644
--- a/src/Lean/Elab/Print.lean
+++ b/src/Lean/Elab/Print.lean
@@ -115,7 +115,7 @@ private def printAxiomsOf (constName : Name) : CommandElabM Unit := do
 
 @[builtinCommandElab «printAxioms»] def elabPrintAxioms : CommandElab
   | `(#print%$tk axioms $id) => withRef tk do
-    let cs ← resolveGlobalConst id.getId
+    let cs ← resolveGlobalConstWithInfos id
     cs.forM printAxiomsOf
   | _ => throwUnsupportedSyntax
 
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 70768d05a7..726d2e83b8 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -113,7 +113,7 @@ where
      `isDescr == true` if the type of `resolvedParserName` is a `ParserDescr`. -/
   resolveParserName (parserName : Name) : ToParserDescrM (List (Name × Bool)) := do
     try
-      let candidates ← resolveGlobalConst parserName
+      let candidates ← resolveGlobalConstWithInfos (← getRef) parserName
       /- Convert `candidates` in a list of pairs `(c, isDescr)`, where `c` is the parser name,
          and `isDescr` is true iff `c` has type `Lean.ParserDescr` or `Lean.TrailingParser` -/
       candidates.filterMap fun c =>
@@ -142,7 +142,7 @@ where
 
   processNullaryOrCat (stx : Syntax) := do
     let id := stx[0].getId.eraseMacroScopes
-    match (← resolveParserName id) with
+    match (← withRef stx[0] <| resolveParserName id) with
     | [(c, true)]      => ensureNoPrec stx; return mkIdentFrom stx c
     | [(c, false)]     => ensureNoPrec stx; `(ParserDescr.parser $(quote c))
     | cs@(_ :: _ :: _) => throwError "ambiguous parser declaration {cs.map (·.1)}"
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 4cf2b183ff..a137891b68 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -317,7 +317,7 @@ private def getElimNameInfo (optElimId : Syntax) (targets : Array Expr) (inducti
     pure (elimName, ← getElimInfo elimName)
   else
     let elimId := optElimId[1]
-    let elimName ← withRef elimId do resolveGlobalConstNoOverload elimId.getId.eraseMacroScopes
+    let elimName ← withRef elimId do resolveGlobalConstNoOverloadWithInfo elimId elimId.getId.eraseMacroScopes
     pure (elimName, ← withRef elimId do getElimInfo elimName)
 
 @[builtinTactic Lean.Parser.Tactic.induction] def evalInduction : Tactic := fun stx => focus do
diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean
index 67d2acbbd7..08d95e729c 100644
--- a/src/Lean/Elab/Tactic/Simp.lean
+++ b/src/Lean/Elab/Tactic/Simp.lean
@@ -51,7 +51,7 @@ private def elabSimpLemmas (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Boo
             -- We use `eraseCore` because the simp lemma for the hypothesis was not added yet
             lemmas ← lemmas.eraseCore arg[1].getId
           else
-            let declName ← resolveGlobalConstNoOverload arg[1].getId
+            let declName ← resolveGlobalConstNoOverloadWithInfo arg[1]
             lemmas ← lemmas.erase declName
         else
           let post :=
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 928395c93f..4fd99fdbb1 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1404,7 +1404,7 @@ def elabScientificLit : TermElab := fun stx expectedType? => do
 
 @[builtinTermElab doubleQuotedName] def elabDoubleQuotedName : TermElab := fun stx _ => do
   match stx[1].isNameLit? with
-  | some val => toExpr (← resolveGlobalConstNoOverload val)
+  | some val => toExpr (← resolveGlobalConstNoOverloadWithInfo stx[1] val)
   | none     => throwIllFormedSyntax
 
 @[builtinTermElab typeOf] def elabTypeOf : TermElab := fun stx _ => do