From 6b1e64d7ea53cdc4a67b6971ef98e5cfa9011ef7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 30 Jan 2020 20:41:10 -0800 Subject: [PATCH] chore: prepare for refactoring --- src/Init/Lean/Parser/Parser.lean | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index ac34a83347..f375d37019 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1733,6 +1733,9 @@ match env.find? constName with | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ => do p ← env.evalConst (Parser leading) constName; pure ⟨leading, p⟩ + | Expr.const `Lean.Parser.Parser _ _ => do + p ← env.evalConst (Parser leading) constName; + pure ⟨leading, p⟩ | Expr.const `Lean.ParserDescr _ _ => do d ← env.evalConst ParserDescr constName; p ← compileParserDescr categories d; @@ -1897,6 +1900,8 @@ match env.find? declName with declareTrailingBuiltinParser env catName declName | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ => declareLeadingBuiltinParser env catName declName + | Expr.const `Lean.Parser.Parser _ _ => + declareLeadingBuiltinParser env catName declName | _ => throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))