diff --git a/src/Lean/Parser/Extension.lean b/src/Lean/Parser/Extension.lean index 645563e2b6..79030f8760 100644 --- a/src/Lean/Parser/Extension.lean +++ b/src/Lean/Parser/Extension.lean @@ -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 := diff --git a/src/Lean/Util/Trace.lean b/src/Lean/Util/Trace.lean index 9f717ae2c3..57d85ef5c9 100644 --- a/src/Lean/Util/Trace.lean +++ b/src/Lean/Util/Trace.lean @@ -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