From a05ca020f43d0dd7d2b06c07398f9cc6b513c49d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 22 Dec 2020 06:52:41 -0800
Subject: [PATCH] chore: prepare to move tactic match parser back to
 `Lean/Parser/Tactic`

---
 src/Lean/Parser/Tactic.lean | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/Lean/Parser/Tactic.lean b/src/Lean/Parser/Tactic.lean
index d386c00df2..2b0975bb22 100644
--- a/src/Lean/Parser/Tactic.lean
+++ b/src/Lean/Parser/Tactic.lean
@@ -15,6 +15,11 @@ builtin_initialize
 @[builtinTacticParser] def «unknown»    := parser! withPosition (ident >> errorAtSavedPos "unknown tactic" true)
 @[builtinTacticParser] def nestedTactic := tacticSeqBracketed
 
+def matchRhs      := Term.hole <|> Term.syntheticHole <|> tacticSeq
+def matchAltsTemp := Term.matchAlts (rhsParser := matchRhs)
+
+@[builtinTacticParser low] def «matchTemp» := parser!:leadPrec "match " >> sepBy1 Term.matchDiscr ", " >> Term.optType >> " with " >> matchAltsTemp
+
 end Tactic
 end Parser
 end Lean