From 54745bda71bd6539e04d208fcdf5e1a1490e2113 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 17 May 2021 15:04:24 -0700 Subject: [PATCH] feat: use new `endPos` field --- src/Init/Prelude.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean index bdb7f2a938..6be4702385 100644 --- a/src/Init/Prelude.lean +++ b/src/Init/Prelude.lean @@ -1784,9 +1784,9 @@ def getPos? (stx : Syntax) (originalOnly := false) : Option String.Pos := partial def getTailPos? (stx : Syntax) (originalOnly := false) : Option String.Pos := match stx, originalOnly with - | atom (SourceInfo.original (pos := pos) ..) val, _ => some (pos.add val.bsize) + | atom (SourceInfo.original (endPos := pos) ..) .., _ => some pos | atom (SourceInfo.synthetic (endPos := pos) ..) _, false => some pos - | ident (SourceInfo.original (pos := pos) ..) val .., _ => some (pos.add val.bsize) + | ident (SourceInfo.original (endPos := pos) ..) .., _ => some pos | ident (SourceInfo.synthetic (endPos := pos) ..) .., false => some pos | node _ args, _ => let rec loop (i : Nat) : Option String.Pos :=