From cc2f84aa5dfef8a374c76cba70be836969058af4 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Feb 2020 11:34:09 -0800
Subject: [PATCH] fix: allow empty sequence at `seq`

---
 src/Init/Lean/Parser/Tactic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 74a6b35c2e..a94b2e5eca 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -37,7 +37,7 @@ def ident' : Parser := ident <|> underscore
 /-
   We must not use the `parser! t` macro here it because it expands into `mkAntiquot ... <|> t`,
   but a tactic parser may start with an antiquotation. -/
-def seq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
+def seq : Parser         := node `Lean.Parser.Tactic.seq $ sepBy tacticParser "; " true
 def nonEmptySeq : Parser := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
 
 @[builtinTacticParser] def «intro»      := parser! nonReservedSymbol "intro " >> optional ident'