michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/blast/imp_extension): do not use the name 'assert'

Browse source 
Closes #994
This commit is contained in:
Daniel Selsam 2016-02-10 14:10:03 -08:00
parent 42b78962f9
commit 3de4ec1a6c
2 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/blast/imp_extension.cpp
View file

@ -24,14 +24,14 @@ 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);
state.assert(h);
state.assert_hyp(h);
}
void imp_extension_state::replay_actions(imp_extension * imp_ext) {
list<hypothesis> const & asserts = reverse(imp_ext->get_asserts());
if (is_nil(asserts)) return;
push();
for_each(asserts, [&](hypothesis const & h) { assert(h); });
for_each(asserts, [&](hypothesis const & h) { assert_hyp(h); });
}
void imp_extension_state::undo_actions(imp_extension * imp_ext) {

2
src/library/blast/imp_extension.h
View file

@ -30,7 +30,7 @@ class imp_extension_state {
public:
virtual void push() =0;
virtual void pop() =0;
virtual void assert(hypothesis const & h) =0;
virtual void assert_hyp(hypothesis const & h) =0;
virtual ~imp_extension_state() {}