From 2df885d9a3fba251fcdebd866eecd65efb130c90 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 13 Oct 2018 11:58:32 -0700 Subject: [PATCH] fix(library/init/lean/parser/token): broken end of comment --- library/init/lean/parser/token.lean | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) diff --git a/library/init/lean/parser/token.lean b/library/init/lean/parser/token.lean index 7f32549ae2..961b87c45e 100644 --- a/library/init/lean/parser/token.lean +++ b/library/init/lean/parser/token.lean @@ -28,9 +28,7 @@ private def finish_comment_block_aux : nat → nat → basic_parser_m unit | nesting (n+1) := str "/-" *> finish_comment_block_aux (nesting + 1) n <|> - str "-/" *> - if nesting = 1 then pure () - else finish_comment_block_aux (nesting - 1) n + str "-/" *> (if nesting = 1 then pure () else finish_comment_block_aux (nesting - 1) n) <|> any *> finish_comment_block_aux nesting n | _ _ := error "unreachable"