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

refactor(library/blast/blast): remove old hack

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-01 12:24:24 -08:00
parent 56d7fc4c23
commit f3648e2ac8
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -197,7 +197,7 @@ class blastenv {
// 1. All href in new_v are in the context of m.
// 2. The context of any (unassigned) mref in new_v must be a subset of the context of m.
// If it is not we force it to be.
// 3. Any (non tmp) local constant occurring in new_v occurs in locals
// 3. Any local constant occurring in new_v occurs in locals
// 4. m does not occur in new_v
state & s = m_benv.m_curr_state;
metavar_decl const * d = s.get_metavar_decl(m);
@ -211,7 +211,7 @@ class blastenv {
ok = false; // failed 1
return false;
}
} else if (is_local(e) && !is_internal_local(e)) {
} else if (is_local(e)) {
if (std::all_of(locals.begin(), locals.end(), [&](expr const & a) {
return mlocal_name(a) != mlocal_name(e); })) {
ok = false; // failed 3