From bb0bfb5742ec69cf3656ce2ae85ac93eb1f4029f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 21 Feb 2020 11:43:45 -0800
Subject: [PATCH] fix: `sepBy`

If parser consumed something, keep error.
---
 src/Init/Lean/Parser/Parser.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index b16b4ecb6c..7fd57d4cbd 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -444,7 +444,8 @@ fun c s =>
   let pos := s.pos;
   let s   := p c s;
   if s.hasError then
-    if pOpt then
+    if s.pos > pos then s
+    else if pOpt then
       let s := s.restore sz pos;
       if s.stackSize - iniSz == 2 && unboxSingleton then
         s.popSyntax