From 5122d88527934de86015cb460319e5e95463fd50 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jan 2020 11:25:24 -0800
Subject: [PATCH] fix: add `SyntaxNodeKind` for seq

---
 src/Init/Lean/Parser/Tactic.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/Init/Lean/Parser/Tactic.lean b/src/Init/Lean/Parser/Tactic.lean
index 73e309d5ff..43fb5f349e 100644
--- a/src/Init/Lean/Parser/Tactic.lean
+++ b/src/Init/Lean/Parser/Tactic.lean
@@ -19,24 +19,22 @@ registerBuiltinDynamicParserAttribute `tacticParser `tactic
 @[inline] def tacticParser {k : ParserKind} (rbp : Nat := 0) : Parser k :=
 categoryParser `tactic rbp
 
-def tacticSeq {k : ParserKind} : Parser k :=
-sepBy1 tacticParser "; " true
-
 namespace Tactic
 
+def seq := parser! sepBy1 tacticParser "; " true
 @[builtinTacticParser] def «intro» := parser! nonReservedSymbol "intro " >> optional ident
 @[builtinTacticParser] def «intros» := parser! nonReservedSymbol "intros " >> many ident
 @[builtinTacticParser] def «assumption» := parser! nonReservedSymbol "assumption"
 @[builtinTacticParser] def «apply» := parser! nonReservedSymbol "apply " >> termParser
-@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> tacticSeq >> "end"
-@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> tacticSeq >> "}"
+@[builtinTacticParser] def nestedTacticBlock := parser! "begin " >> seq >> "end"
+@[builtinTacticParser] def nestedTacticBlockCurly := parser! "{" >> seq >> "}"
 @[builtinTacticParser] def orelse := tparser! pushLeading >> " <|> " >> tacticParser 1
 
 end Tactic
 
 namespace Term
 
-@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> tacticSeq >> "end"
+@[builtinTermParser] def tacticBlock := parser! symbol "begin " appPrec >> Tactic.seq >> "end"
 
 end Term