From e535ebcce8d467f0372ef6ac4098ae643f7b256e Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Thu, 2 Aug 2018 14:16:25 -0700 Subject: [PATCH] fix(frontends/lean/util): remove reference to obsolete match syntax --- src/frontends/lean/util.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/util.cpp b/src/frontends/lean/util.cpp index 75da137cb3..bbaa6f9ccc 100644 --- a/src/frontends/lean/util.cpp +++ b/src/frontends/lean/util.cpp @@ -88,8 +88,8 @@ name remove_root_prefix(name const & n) { return n.replace_prefix(get_root_tk(), name()); } -bool is_eqn_prefix(parser & p, bool bar_only = false) { - return p.curr_is_token(get_bar_tk()) || (!bar_only && p.curr_is_token(get_comma_tk())); +bool is_eqn_prefix(parser & p, bool) { + return p.curr_is_token(get_bar_tk()); } // Return the local levels in \c ls that are not associated with variables