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

chore: remove temporary hacks

Browse source
This commit is contained in:
Leonardo de Moura 2020-09-19 14:21:38 -07:00
parent a96e5d4bcd
commit 17d4117637
2 changed files with 1 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Parser/Extension.lean
View file

@ -87,7 +87,6 @@ def throwUnknownParserCategory {α} (catName : Name) : ExceptT String Id α :=
throw ("unknown parser category '" ++ toString catName ++ "'")
abbrev getCategory (categories : ParserCategories) (catName : Name) : Option ParserCategory :=
let catName := if catName == `syntax then `stx else catName; -- temporary hack
categories.find? catName
def addLeadingParser (categories : ParserCategories) (catName : Name) (parserName : Name) (p : Parser) : Except String ParserCategories :=

2
src/Lean/Util/Trace.lean
View file

@ -133,6 +133,6 @@ new_frontend
namespace Lean
-- macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
macro:max "trace!" id:term:max msg:term : term => `(trace $id fun _ => ($msg : MessageData))
end Lean