From fa338c188502c392224150b4a4e1a67515e240cf Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 10 Oct 2020 10:58:44 -0700
Subject: [PATCH] refactor: move `resolveGlobalName` to `Lean` namespace

---
 src/Lean/Elab/Alias.lean       | 36 -------------------------------
 src/Lean/Elab/Command.lean     |  2 +-
 src/Lean/Elab/ResolveName.lean | 39 +++++++++++++++++++++++++++++++---
 src/Lean/Elab/Term.lean        |  2 +-
 4 files changed, 38 insertions(+), 41 deletions(-)

diff --git a/src/Lean/Elab/Alias.lean b/src/Lean/Elab/Alias.lean
index 3a682f5741..707593b001 100644
--- a/src/Lean/Elab/Alias.lean
+++ b/src/Lean/Elab/Alias.lean
@@ -7,40 +7,4 @@ import Lean.Environment
 
 namespace Lean
 
-/-!
-  We use aliases to implement the `export <id> (<id>+)` command.
-  An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`. -/
-
-abbrev AliasState := SMap Name (List Name)
-abbrev AliasEntry := Name × Name
-
-def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
-match s.find? e.1 with
-| none    => s.insert e.1 [e.2]
-| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
-
-def mkAliasExtension : IO (SimplePersistentEnvExtension AliasEntry AliasState) :=
-registerSimplePersistentEnvExtension {
-  name          := `aliasesExt,
-  addEntryFn    := addAliasEntry,
-  addImportedFn := fun es => (mkStateFromImportedEntries addAliasEntry {} es).switch
-}
-
-@[init mkAliasExtension]
-constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := arbitrary _
-
-/- Add alias `a` for `e` -/
-@[export lean_add_alias]
-def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
-aliasExtension.addEntry env (a, e)
-
-def getAliases (env : Environment) (a : Name) : List Name :=
-match (aliasExtension.getState env).find? a with
-| none    => []
-| some es => es
-
--- slower, but only used in the pretty printer
-def getRevAliases (env : Environment) (e : Name) : List Name :=
-(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
-
 end Lean
diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean
index 98b68a46d0..b5d1a7043f 100644
--- a/src/Lean/Elab/Command.lean
+++ b/src/Lean/Elab/Command.lean
@@ -397,7 +397,7 @@ def resolveNamespace (id : Name) : CommandElabM Name := do
 env           ← getEnv;
 currNamespace ← getCurrNamespace;
 openDecls ← getOpenDecls;
-match Elab.resolveNamespace env currNamespace openDecls id with
+match Lean.resolveNamespace env currNamespace openDecls id with
 | some ns => pure ns
 | none    => throwError ("unknown namespace '" ++ id ++ "'")
 
diff --git a/src/Lean/Elab/ResolveName.lean b/src/Lean/Elab/ResolveName.lean
index 856d935fcb..d988a5e7cb 100644
--- a/src/Lean/Elab/ResolveName.lean
+++ b/src/Lean/Elab/ResolveName.lean
@@ -6,10 +6,44 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 import Lean.Data.OpenDecl
 import Lean.Hygiene
 import Lean.Modifiers
-import Lean.Elab.Alias
 
 namespace Lean
-namespace Elab
+
+/-!
+  We use aliases to implement the `export <id> (<id>+)` command.
+  An `export A (x)` in the namespace `B` produces an alias `B.x ~> A.x`. -/
+
+abbrev AliasState := SMap Name (List Name)
+abbrev AliasEntry := Name × Name
+
+def addAliasEntry (s : AliasState) (e : AliasEntry) : AliasState :=
+match s.find? e.1 with
+| none    => s.insert e.1 [e.2]
+| some es => if es.elem e.2 then s else s.insert e.1 (e.2 :: es)
+
+def mkAliasExtension : IO (SimplePersistentEnvExtension AliasEntry AliasState) :=
+registerSimplePersistentEnvExtension {
+  name          := `aliasesExt,
+  addEntryFn    := addAliasEntry,
+  addImportedFn := fun es => (mkStateFromImportedEntries addAliasEntry {} es).switch
+}
+
+@[init mkAliasExtension]
+constant aliasExtension : SimplePersistentEnvExtension AliasEntry AliasState := arbitrary _
+
+/- Add alias `a` for `e` -/
+@[export lean_add_alias]
+def addAlias (env : Environment) (a : Name) (e : Name) : Environment :=
+aliasExtension.addEntry env (a, e)
+
+def getAliases (env : Environment) (a : Name) : List Name :=
+match (aliasExtension.getState env).find? a with
+| none    => []
+| some es => es
+
+-- slower, but only used in the pretty printer
+def getRevAliases (env : Environment) (e : Name) : List Name :=
+(aliasExtension.getState env).fold (fun as a es => if List.contains es e then a :: as else as) []
 
 /- Global name resolution -/
 
@@ -114,5 +148,4 @@ else match resolveNamespaceUsingScope env id ns with
     | some n => some n
     | none   => none
 
-end Elab
 end Lean
diff --git a/src/Lean/Elab/Term.lean b/src/Lean/Elab/Term.lean
index 1b4d5ff153..de18c1f598 100644
--- a/src/Lean/Elab/Term.lean
+++ b/src/Lean/Elab/Term.lean
@@ -1268,7 +1268,7 @@ def resolveGlobalName (n : Name) : TermElabM (List (Name × List String)) := do
 env ← getEnv;
 currNamespace ← getCurrNamespace;
 openDecls ← getOpenDecls;
-pure (Lean.Elab.resolveGlobalName env currNamespace openDecls n)
+pure (Lean.resolveGlobalName env currNamespace openDecls n)
 
 /- Similar to `resolveGlobalName`, but discard any candidate whose `fieldList` is not empty. -/
 def resolveGlobalConst (n : Name) : TermElabM (List Name) := do