From ffca6975f2c1645e4733fbe8a7e572adf0cd8903 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 14 Feb 2022 15:39:21 -0800 Subject: [PATCH] chore: remove bootstrapping workarounds --- src/Lean/Elab/Match.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 6c9d2f0eed..4c877cb3a9 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -850,16 +850,10 @@ private def elabMatchAux (generalizing? : Option Bool) (discrStxs : Array Syntax -- leading_parser "match " >> optional generalizingParam >> optional motive >> sepBy1 matchDiscr ", " >> " with " >> ppDedent matchAlts private def getDiscrs (matchStx : Syntax) : Array Syntax := - if matchStx[3].isNone then -- HACK for bootstrapping issues - matchStx[2].getSepArgs - else - matchStx[3].getSepArgs + matchStx[3].getSepArgs private def getMatchOptMotive (matchStx : Syntax) : Syntax := - if !matchStx[2].isNone && matchStx[2][0].isOfKind ``Lean.Parser.Term.matchDiscr then -- HACK for bootstrapping issues - mkNullNode - else - matchStx[2] + matchStx[2] private def expandNonAtomicDiscrs? (matchStx : Syntax) : TermElabM (Option Syntax) := let matchOptMotive := getMatchOptMotive matchStx