From 78b1d4279b6fee171aa6d3fac70ba04617aef169 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Nov 2015 16:35:50 -0800 Subject: [PATCH] fix(library/blast/state): compilation problems in debug mode --- src/library/blast/state.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index bba985a4e..c2da366c4 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -322,7 +322,6 @@ expr state::instantiate_urefs_mrefs(expr const & e) { bool state::check_hypothesis(expr const & e, branch const & b, unsigned hidx, hypothesis const & h) const { lean_assert(closed(e)); for_each(e, [&](expr const & n, unsigned) { - lean_assert(!blast::is_local(n)); if (is_href(n)) { lean_assert(h.depends_on(n)); lean_assert(b.hidx_depends_on(hidx, href_index(n))); @@ -344,7 +343,6 @@ bool state::check_hypothesis(branch const & b, unsigned hidx, hypothesis const & bool state::check_target(branch const & b) const { lean_assert(closed(b.get_target())); for_each(b.get_target(), [&](expr const & n, unsigned) { - lean_assert(!blast::is_local(n)); if (is_href(n)) { lean_assert(b.target_depends_on(n)); } else if (is_mref(n)) {