From cb55ffae94ff59a9802ef60cbf89f71057503268 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 28 Sep 2020 14:58:31 -0700
Subject: [PATCH] chore: add new tactic syntax kind

---
 src/Lean/Parser/Tactic.lean | 1 -
 src/Lean/Parser/Term.lean   | 4 ++++
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index 59e813d3b3..e1a44fc336 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -74,7 +74,6 @@ def matchAlts : Parser := group $ withPosition $ (optional "| ") >> sepBy1 match
 
 def withIds : Parser := optional (" with " >> many1 ident')
 @[builtinTacticParser] def «injection»  := parser! nonReservedSymbol "injection " >> termParser >> withIds
-def seq1 := node `Lean.Parser.Tactic.seq $ sepBy1 tacticParser "; " true
 @[builtinTacticParser] def paren        := parser! "(" >> seq1 >> ")"
 @[builtinTacticParser] def nestedTactic := tacticSeqBracketed
 @[builtinTacticParser] def orelse := tparser!:2 " <|> " >> tacticParser 1
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 346e4b0cf4..7baa65f125 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -28,6 +28,10 @@ def tacticSeqBracketed : Parser :=
   parser! "{" >> sepBy tacticParser "; " true >> "}"
 def tacticSeq :=
   nodeWithAntiquot "tacticSeq" `Lean.Parser.Tactic.tacticSeq $ tacticSeqBracketed <|> tacticSeq1Indented
+
+/- Raw sequence for quotation and grouping -/
+def seq1 := parser! sepBy1 tacticParser "; " true
+
 end Tactic
 
 def darrow : Parser := " => "