From 0be31c14ec00fc35e117bb2c00d85a438eeedb00 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 22 Jan 2020 12:05:12 -0800 Subject: [PATCH] fix: workaround for term parser antiquotation issue @Kha this is a temporary workaround. We should discuss how to cleanup in the next Dev meeting. --- src/Init/Lean/Parser/Parser.lean | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 8735fb1dc6..1d8618e5a9 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1767,7 +1767,10 @@ private def catNameToString : Name → String | n => n.toString def categoryParserFnImpl (catName : Name) : ParserFn leading := -orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName) +if catName != `term then + orelseFn (mkAntiquot (catNameToString catName) none false).fn (categoryParserFnImplAux catName) +else + categoryParserFnImplAux catName @[init] def setCategoryParserFnRef : IO Unit := categoryParserFnRef.set categoryParserFnImpl