From ecb787529ad02bf3dcfb95d7ed9392d438452d09 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Mon, 1 Aug 2022 04:19:39 -0400
Subject: [PATCH] refactor: rename ref to declName

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

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 8859c69785..e4b014f66a 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1612,7 +1612,7 @@ inductive LeadingIdentBehavior where
   The method `termParser prec` is equivalent to the method above.
 -/
 structure ParserCategory where
-  ref      : Name
+  declName : Name
   kinds    : SyntaxNodeKindSet := {}
   tables   : PrattParsingTables := {}
   behavior : LeadingIdentBehavior
diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean
index be3878aa9c..5d2555cb5e 100644
--- a/src/Lean/Parser/Extension.lean
+++ b/src/Lean/Parser/Extension.lean
@@ -46,9 +46,9 @@ private def addParserCategoryCore (categories : ParserCategories) (catName : Nam
 
 /-- All builtin parser categories are Pratt's parsers -/
 
-private def addBuiltinParserCategory (catName ref : Name) (behavior : LeadingIdentBehavior) : IO Unit := do
+private def addBuiltinParserCategory (catName declName : Name) (behavior : LeadingIdentBehavior) : IO Unit := do
   let categories ← builtinParserCategoriesRef.get
-  let categories ← IO.ofExcept $ addParserCategoryCore categories catName { ref, behavior }
+  let categories ← IO.ofExcept $ addParserCategoryCore categories catName { declName, behavior }
   builtinParserCategoriesRef.set categories
 
 namespace ParserExtension
@@ -162,10 +162,10 @@ def ParserExtension.addEntryImpl (s : State) (e : Entry) : State :=
     | _                => unreachable!
   | Entry.kind k =>
     { s with kinds := s.kinds.insert k }
-  | Entry.category catName ref behavior =>
+  | Entry.category catName declName behavior =>
     if s.categories.contains catName then s
     else { s with
-           categories := s.categories.insert catName { ref, behavior } }
+           categories := s.categories.insert catName { declName, behavior } }
   | Entry.parser catName declName leading parser prio =>
     match addParser s.categories catName declName leading parser prio with
     | Except.ok categories => { s with categories }