From 5765a1160df4b0aac32d5b59594ec11ea9ed49ce Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 4 Jun 2020 10:07:48 -0700 Subject: [PATCH] fix: `Parser` ==> `TrailingParser` --- src/Lean/Parser/Parser.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Parser/Parser.lean b/src/Lean/Parser/Parser.lean index 0876df33d6..23071ae7c6 100644 --- a/src/Lean/Parser/Parser.lean +++ b/src/Lean/Parser/Parser.lean @@ -1105,7 +1105,7 @@ checkRbpLt (upper + 1) errorMsg checkRbpLe prec >> leadingNode n p /- Version of `trailingNode` which uses `checkRbpLt` -/ -@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : Parser := +@[inline] def trailingNodePrec (n : SyntaxNodeKind) (prec : Nat) (p : Parser) : TrailingParser := checkRbpLt prec >> trailingNode n p def mkAtomicInfo (k : String) : ParserInfo :=