From 091000462d2b287bb6fed49e7b987c2546563b81 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 28 Aug 2020 09:43:23 -0700 Subject: [PATCH] chore: remove unnecessary node --- src/Lean/Elab/Tactic/Match.lean | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean index dfb4fd3cc9..147e46bb03 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/src/Lean/Elab/Tactic/Match.lean @@ -44,8 +44,7 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM pure (matchTerm, s.cases) def mkTacticSeq (ref : Syntax) (tacs : Array Syntax) : Syntax := -let seq := mkSepStx tacs (mkAtomFrom ref "; "); -Syntax.node `Lean.Parser.Tactic.seq #[seq] +mkSepStx tacs (mkAtomFrom ref "; ") @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic := fun stx => do