From 76c27c9aa48cc4e9b79aeb0874968ea970ba7554 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 19 Jul 2019 11:11:50 -0700
Subject: [PATCH] feat(library/init/lean/syntax): update `preresolved` field

The `Nat` is for handling the ambiguous `.` notation in Lean during
preresolution. Recall that `x.y` may represent a hierarchical name or
a "field access".
---
 library/init/lean/syntax.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/library/init/lean/syntax.lean b/library/init/lean/syntax.lean
index 98748489f2..ca093a51f5 100644
--- a/library/init/lean/syntax.lean
+++ b/library/init/lean/syntax.lean
@@ -34,7 +34,7 @@ inductive Syntax (α : Type := Unit)
 | missing {} : Syntax
 | node   (kind : SyntaxNodeKind) (args : Array Syntax) : Syntax
 | atom   {} (info : Option SourceInfo) (val : String) : Syntax
-| ident  {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List Name) : Syntax
+| ident  {} (info : Option SourceInfo) (rawVal : Substring) (val : Name) (preresolved : List (Nat × Name)) : Syntax
 | other  : α → Syntax
 
 instance stxInh {α} : Inhabited (Syntax α) :=