From 8c431bdb20b09254707943393202aa067eb36d5b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 4 Dec 2015 08:34:20 -0800 Subject: [PATCH] chore(library/blast/imp_extension): fix unused argument warning --- src/library/blast/imp_extension.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/imp_extension.cpp b/src/library/blast/imp_extension.cpp index 65bdc68eb..470c9809e 100644 --- a/src/library/blast/imp_extension.cpp +++ b/src/library/blast/imp_extension.cpp @@ -20,7 +20,7 @@ imp_extension * imp_extension::clone() { return new imp_extension(this); } -void imp_extension::hypothesis_activated(hypothesis const & h, hypothesis_idx hidx) { +void imp_extension::hypothesis_activated(hypothesis const & h, hypothesis_idx) { imp_extension_state & state = get_imp_extension_state(m_state_id); if (is_nil(m_asserts)) state.push(); m_asserts = cons(h, m_asserts);