From a1f079227ba5fb98676ca4717d4f0b790343bd27 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Dec 2019 19:41:16 -0800
Subject: [PATCH] chore: prepare to move `ParserKind`

---
 src/Init/Lean/Parser/Parser.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean
index f4201dbc30..00115a7f09 100644
--- a/src/Init/Lean/Parser/Parser.lean
+++ b/src/Init/Lean/Parser/Parser.lean
@@ -1461,7 +1461,7 @@ registerAttribute {
      match decl.type with
      | Expr.const `Lean.Parser.TrailingParser _ _ =>
        declareTrailingBuiltinParser env refDeclName declName
-     | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.Parser.ParserKind.leading _ _) _ =>
+     | Expr.app (Expr.const `Lean.Parser.Parser _ _) (Expr.const `Lean.ParserKind.leading _ _) _ =>
        declareLeadingBuiltinParser env refDeclName declName
      | _ =>
        throw (IO.userError ("unexpected parser type at '" ++ toString declName ++ "' (`Parser` or `TrailingParser` expected"))