From b61eb3ea0c1bbb917725279e4e91fe5d7ec9c151 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 18 Nov 2015 18:01:58 -0800 Subject: [PATCH] fix(library/blast): compilation errors in debug mode --- src/library/blast/state.cpp | 2 +- src/library/blast/subst_action.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/library/blast/state.cpp b/src/library/blast/state.cpp index 41d12514ef..7692fd6bc0 100644 --- a/src/library/blast/state.cpp +++ b/src/library/blast/state.cpp @@ -712,7 +712,7 @@ branch_extension & state::get_extension(unsigned extid) { branch_extension * ext = get_extension_manager().get_initial(extid)->clone();; ext->inc_ref(); m_branch.m_extensions[extid] = ext; - lean_assert(ext.get_rc() == 1); + lean_assert(ext->get_rc() == 1); ext->initialized(); m_branch.m_active.for_each([&](hypothesis_idx hidx) { hypothesis const * h = get_hypothesis_decl(hidx); diff --git a/src/library/blast/subst_action.cpp b/src/library/blast/subst_action.cpp index c4c250f1f9..ae0c5cbc34 100644 --- a/src/library/blast/subst_action.cpp +++ b/src/library/blast/subst_action.cpp @@ -74,7 +74,7 @@ bool subst_core(hypothesis_idx hidx) { new_target = instantiate(new_target, lhs); s.push_proof_step(new subst_proof_step_cell(target, h->get_self(), rhs, dep)); s.set_target(new_target); - lean_verify(intros_action(num)); + intros_action(num); } lean_verify(s.del_hypothesis(hidx)); lean_verify(s.del_hypothesis(href_index(rhs)));