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"