From 6a767a66a13c588cce3829bf1de00a1830883843 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Sat, 23 Jul 2022 23:01:52 +0200
Subject: [PATCH] perf: reduce Lean.Parser.Basic imports

---
 src/Lean/Parser/Basic.lean     | 6 ------
 src/Lean/Parser/Extension.lean | 3 +++
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 233f38d64f..878bdb99df 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -8,10 +8,7 @@ import Lean.Data.Position
 import Lean.Syntax
 import Lean.ToExpr
 import Lean.Environment
-import Lean.Attributes
 import Lean.Message
-import Lean.Compiler.InitAttr
-import Lean.ResolveName
 
 /-!
 # Basic Lean parser infrastructure
@@ -135,9 +132,6 @@ structure ParserContext extends InputContext, ParserModuleContext where
   savedPos?          : Option String.Pos := none
   forbiddenTk?       : Option Token := none
 
-def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
-  ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
-
 structure Error where
   unexpected : String := ""
   expected : List String := []
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index 5472544f43..d6b791f28e 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -622,6 +622,9 @@ def withOpenDeclFn (p : ParserFn) : ParserFn := fun c s =>
   fn   := withOpenDeclFn  p.fn
 }
 
+def ParserContext.resolveName (ctx : ParserContext) (id : Name) : List (Name × List String) :=
+  ResolveName.resolveGlobalName ctx.env ctx.currNamespace ctx.openDecls id
+
 def parserOfStackFn (offset : Nat) : ParserFn := fun ctx s => Id.run do
   let stack := s.stxStack
   if stack.size < offset + 1 then