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

fix(library/blast/forward/ematch): typo

Browse source
This commit is contained in:
Daniel Selsam 2015-12-01 14:27:46 -08:00 committed by Leonardo de Moura
parent cc8a5581d6
commit 42dcbebd1c
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

@ -191,7 +191,7 @@ struct ematch_fn {
expr it = t;
do {
expr const & it_fn = get_app_fn(it);
if (m_cc.is_congr_root(R, t) && m_ctx->is_def_eq(it_fn, fn) &&
if (m_cc.is_congr_root(R, it) && m_ctx->is_def_eq(it_fn, fn) &&
get_app_num_args(it) == p_args.size()) {
t_fn = it_fn;
candidates.push_back(it);