From 4101ba640cfddd1ec7561c82ebc4c75403cfb5df Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 16 Feb 2020 11:17:53 -0800
Subject: [PATCH] chore: add `resolveGlobalName` method

---
 src/Init/Lean/Elab/Quotation.lean |  6 ++----
 src/Init/Lean/Elab/Term.lean      | 12 ++++++++----
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 8515ab3a1e..7a2baf8c4f 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/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))
diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index d4bd8e75bd..661a945bda 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/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