From 09687f70af152d6de86f40b41985fc7aa4cfd96d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Sep 2016 19:50:30 -0700 Subject: [PATCH] chore(frontends/lean/builtin_exprs): fix compilation warning --- src/frontends/lean/builtin_exprs.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index b1b296174b..fae0335d64 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -414,7 +414,7 @@ static expr parse_sorry(parser & p, unsigned, expr const *, pos_info const & pos return p.mk_sorry(pos); } -static expr parse_rparen(parser & p, unsigned, expr const * args, pos_info const & pos) { +static expr parse_rparen(parser & /* p */, unsigned, expr const * args, pos_info const & /* pos */) { return args[0]; }