From c4d7eb7949dad2cbafa7cd1603e0a0b5f34169cf Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 29 May 2018 16:42:52 +0200
Subject: [PATCH] feat(init/lean/parser/macro): global names can be overloaded

---
 library/init/lean/parser/macro.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/init/lean/parser/macro.lean b/library/init/lean/parser/macro.lean
index c9d9cacc68..8780b5bd44 100644
--- a/library/init/lean/parser/macro.lean
+++ b/library/init/lean/parser/macro.lean
@@ -34,8 +34,8 @@ def run' {r σ α} (cfg : r) (st : σ): parse_m r σ α → except string α :=
 end parse_m
 
 structure resolved :=
--- local or global
-(decl : syntax_id ⊕ name)
+-- local or (overloaded) global
+(decl : syntax_id ⊕ list name)
 /- prefix of the reference that corresponds to the decl. All trailing name components
    are field accesses. -/
 («prefix» : name)