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

fix(library/blast/state): incorrect assertions

Browse source
This commit is contained in:
Leonardo de Moura 2015-11-12 16:28:09 -08:00
parent 98f91931bf
commit 1e436b8b3e
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -298,7 +298,6 @@ public:
}
level const * get_uref_assignment(level const & l) const {
lean_assert(is_uref_assigned(l));
return m_uassignment.find(uref_index(l));
}
@ -316,7 +315,6 @@ public:
bool has_assigned_uref(levels const & ls) const;
expr const * get_mref_assignment(expr const & e) const {
lean_assert(is_mref(e));
return m_eassignment.find(mref_index(e));
}