From 532efde6659ff62fbe361fbf28df050405ac4fa9 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 9 Sep 2016 18:01:39 -0700 Subject: [PATCH] chore(library/local_context): fix warning --- src/library/local_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 20cf7ab374..2e66b435c5 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -38,9 +38,10 @@ name mk_local_decl_name() { return mk_tagged_fresh_name(*g_local_prefix); } +DEBUG_CODE( static bool is_local_decl_name(name const & n) { return is_tagged_by(n, *g_local_prefix); -} +}) static expr mk_local_ref(name const & n, name const & pp_n, binder_info const & bi) { return mk_local(n, pp_n, *g_dummy_type, bi);