max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove workaround

Browse source
This commit is contained in:
Leonardo de Moura 2020-12-22 07:19:33 -08:00
parent c0e3381a4d
commit b254aafea0
1 changed files with 1 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/Lean/Elab/Tactic/Basic.lean
View file

@ -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