From b254aafea0fd90d6cc1919a615aba670994d47bd Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 22 Dec 2020 07:19:33 -0800 Subject: [PATCH] chore: remove workaround --- src/Lean/Elab/Tactic/Basic.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean index 92caeb281a..7f56adeb45 100644 --- a/src/Lean/Elab/Tactic/Basic.lean +++ b/src/Lean/Elab/Tactic/Basic.lean @@ -325,9 +325,7 @@ private def introStep (n : Name) : TacticM Unit := | `(tactic| intro $h:ident) => introStep h.getId | `(tactic| intro _) => introStep `_ | `(tactic| intro $pat:term) => do - let m ← `(match h with | $pat:term => _) - let m := m.setKind ``Lean.Parser.Tactic.match - let stxNew ← `(tactic| intro h; $m; clear h) + let stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h) withMacroExpansion stx stxNew $ evalTactic stxNew | `(tactic| intro $hs:term*) => do let h0 := hs.get! 0