From 770ca546be7bfdffc0d5359e1704275af8a8e22d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 16 Nov 2015 19:02:02 -0800 Subject: [PATCH] fix(library/norm_num): unused variables warnings --- src/library/norm_num.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/norm_num.cpp b/src/library/norm_num.cpp index 2b1be62ac2..9d3dcb851a 100644 --- a/src/library/norm_num.cpp +++ b/src/library/norm_num.cpp @@ -671,7 +671,7 @@ expr norm_num_context::mk_norm_eq_pos_add_neg(expr & s_lhs, expr & s_rhs, expr & } // returns a proof that s_lhs + s_rhs = rhs, where all are nonneg normalized numerals -expr norm_num_context::mk_norm_eq_pos_add_pos(expr & s_lhs, expr & s_rhs, expr & rhs) { +expr norm_num_context::mk_norm_eq_pos_add_pos(expr & s_lhs, expr & s_rhs, expr & DEBUG_CODE(rhs)) { lean_assert(!is_neg_app(s_lhs)); lean_assert(!is_neg_app(s_rhs)); lean_assert(!is_neg_app(rhs)); @@ -718,7 +718,7 @@ expr norm_num_context::mk_norm_eq_pos_mul_neg(expr & s_lhs, expr & s_rhs, expr & } // returns a proof that s_lhs + s_rhs = rhs, where all are nonneg normalized numerals -expr norm_num_context::mk_norm_eq_pos_mul_pos(expr & s_lhs, expr & s_rhs, expr & rhs) { +expr norm_num_context::mk_norm_eq_pos_mul_pos(expr & s_lhs, expr & s_rhs, expr & DEBUG_CODE(rhs)) { lean_assert(!is_neg_app(s_lhs)); lean_assert(!is_neg_app(s_rhs)); lean_assert(!is_neg_app(rhs));