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

chore: remove obsolete workaround

Browse source
This commit is contained in:
Sebastian Ullrich 2022-05-01 11:47:11 +02:00
parent 4174643dbd
commit 952abbf16b
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/Lean/PrettyPrinter/Parenthesizer.lean
View file

@ -336,12 +336,8 @@ def parserOfStack.parenthesizer (offset : Nat) (prec : Nat := 0) : Parenthesizer
@[builtinCategoryParenthesizer term]
def term.parenthesizer : CategoryParenthesizer | prec => do
let stx ← getCur
-- this can happen at `termParser <|> many1 commandParser` in `Term.stxQuot`
if stx.getKind == nullKind then
throwBacktrack
else do
maybeParenthesize `term true (fun stx => Unhygienic.run `(($stx))) prec $
parenthesizeCategoryCore `term prec
maybeParenthesize `term true (fun stx => Unhygienic.run `(($stx))) prec $
parenthesizeCategoryCore `term prec
@[builtinCategoryParenthesizer tactic]
def tactic.parenthesizer : CategoryParenthesizer | prec => do