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

fix(library/blast/forward/ematch): must used the right type_context

Browse source
This commit is contained in:
Leonardo de Moura 2016-02-23 13:32:34 -08:00
parent 2a35c0f49b
commit 494b88e103
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/blast/forward/ematch.cpp
View file

@ -638,7 +638,7 @@ struct ematch_fn {
expr const & p0 = ps[0];
buffer<expr> p0_args;
expr const & f = get_app_args(p0, p0_args);
name const & R = is_prop(p0) ? get_iff_name() : get_eq_name();
name const & R = m_ctx->is_prop(p0) ? get_iff_name() : get_eq_name();
unsigned gmt = m_cc.get_gmt();
if (auto s = m_inst_ext.get_apps().find(head_index(f))) {
s->for_each([&](expr const & t) {