From 6672cc2a342b8f6bfce35bb636bc0745ff110a47 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 May 2018 17:15:12 -0700
Subject: [PATCH] fix(library/init/lean/parser/parser): bug

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

diff --git a/library/init/lean/parser/parser.lean b/library/init/lean/parser/parser.lean
index 5e5e5aa7ae..2574b9e91b 100644
--- a/library/init/lean/parser/parser.lean
+++ b/library/init/lean/parser/parser.lean
@@ -366,7 +366,7 @@ def many1 (p : parser α) : parser (list α) :=
 do r ← remaining, many1_aux p r
 
 def many (p : parser α) : parser (list α) :=
-many1 p <* eps
+many1 p <|> return []
 
 def many1_aux' (p : parser α) : nat → parser unit
 | 0     := p >> return ()
@@ -376,7 +376,7 @@ def many1' (p : parser α) : parser unit :=
 do r ← remaining, many1_aux' p r
 
 def many' (p : parser α) : parser unit :=
-many1' p <* eps
+many1' p <|> return ()
 
 def eoi : parser unit :=
 λ it, if it.remaining = 0 then ok_eps () it { pos := it.offset }