From e51b07801537455a3ce18ff6412e5fe8923f4527 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 24 Sep 2022 13:45:50 -0700
Subject: [PATCH] fix: incorrect annotations

---
 src/Lean/Data/Parsec.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/Lean/Data/Parsec.lean b/src/Lean/Data/Parsec.lean
index 5e4c889a94..29eaaaa4c7 100644
--- a/src/Lean/Data/Parsec.lean
+++ b/src/Lean/Data/Parsec.lean
@@ -69,7 +69,7 @@ def eof : Parsec Unit := fun it =>
   else
     success it ()
 
-@[inline]
+@[specialize]
 partial def manyCore (p : Parsec α) (acc : Array α) : Parsec $ Array α :=
   (do manyCore p (acc.push $ ←p))
   <|> pure acc
@@ -80,7 +80,7 @@ def many (p : Parsec α) : Parsec $ Array α := manyCore p #[]
 @[inline]
 def many1 (p : Parsec α) : Parsec $ Array α := do manyCore p #[←p]
 
-@[inline]
+@[specialize]
 partial def manyCharsCore (p : Parsec Char) (acc : String) : Parsec String :=
   (do manyCharsCore p (acc.push $ ←p))
   <|> pure acc