From 7654fa34e0e37ba80fd24aecfc1e4cccff3a19cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 3 Nov 2020 10:01:18 -0800
Subject: [PATCH] feat: add `tacticSeq`

@Kha This is a small hack to allow users to use `tacticSeq` in
`syntax` command. Example:
```
syntax "repeat" tacticSeq : tactic
```
---
 src/Lean/Parser/Tactic.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 5a328e9cd8..551aa09b6a 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -9,6 +9,10 @@ namespace Lean
 namespace Parser
 namespace Tactic
 
+-- Auxiliary parsing category just to expose the nonterminal `tacticSeq` to the `syntax` command
+builtin_initialize
+  registerBuiltinParserAttribute `builtinTacticSeqParser `tacticSeq
+
 def underscoreFn : ParserFn := fun c s =>
   let s   := symbolFn "_" c s;
   let stx := s.stxStack.back;