chore: add resolveGlobalName method

src/Init/Lean/Elab/Quotation.lean

@@ -104,10 +104,8 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
 | Syntax.ident info rawVal val preresolved => do
   -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation).
   -- See the paper for details.
-  env           ← getEnv;
-  currNamespace ← getCurrNamespace;
-  openDecls     ← getOpenDecls;
-  let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved;
+  r ← resolveGlobalName val;
+  let preresolved := r ++ preresolved;
   let val := quote val;
   -- `scp` is bound in stxQuot.expand
   `(Syntax.ident none $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved))

src/Init/Lean/Elab/Term.lean

@@ -1043,6 +1043,12 @@ candidates.foldlM
     pure $ (const, projs) :: result)
   []
 
+def resolveGlobalName (n : Name) : TermElabM (List (Name × List String)) := do
+env ← getEnv;
+currNamespace ← getCurrNamespace;
+openDecls ← getOpenDecls;
+pure (Lean.Elab.resolveGlobalName env currNamespace openDecls n)
+
 def resolveName (ref : Syntax) (n : Name) (preresolved : List (Name × List String)) (explicitLevels : List Level) : TermElabM (List (Expr × List String)) := do
 result? ← resolveLocalName n;
 match result? with
@@ -1060,10 +1066,8 @@ match result? with
     mkConsts ref candidates explicitLevels
   };
   if preresolved.isEmpty then do
-    env           ← getEnv;
-    currNamespace ← getCurrNamespace;
-    openDecls     ← getOpenDecls;
-    process (resolveGlobalName env currNamespace openDecls n)
+    r ← resolveGlobalName n;
+    process r
   else
     process preresolved