From c0cf54e8d4378d940ac55c1ccb160532d352d743 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 21 Sep 2015 16:21:21 -0700 Subject: [PATCH] chore(library/blast): fix compilation warning --- src/library/blast/expr.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/library/blast/expr.cpp b/src/library/blast/expr.cpp index 14b462d42..dbb2feb0e 100644 --- a/src/library/blast/expr.cpp +++ b/src/library/blast/expr.cpp @@ -121,11 +121,18 @@ scope_hash_consing::~scope_hash_consing() { g_lref_array = reinterpret_cast(m_lref_array); } +#ifdef LEAN_DEBUG static bool is_cached(level const & l) { lean_assert(g_level_table); return g_level_table->find(l) != g_level_table->end(); } +static bool is_cached(expr const & l) { + lean_assert(g_expr_table); + return g_expr_table->find(l) != g_expr_table->end(); +} +#endif + static level cache(level const & l) { lean_assert(g_level_table); auto r = g_level_table->find(l); @@ -135,11 +142,6 @@ static level cache(level const & l) { return l; } -static bool is_cached(expr const & l) { - lean_assert(g_expr_table); - return g_expr_table->find(l) != g_expr_table->end(); -} - static expr cache(expr const & e) { lean_assert(g_expr_table); auto r = g_expr_table->find(e);