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

fix(library/blast/forward/ematch): bug in match_leaf

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-16 10:51:00 -08:00
parent a883101a3b
commit 98319139d9
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

@ -355,9 +355,9 @@ struct ematch_fn {
if (R == get_eq_name() && m_cc.eq_class_heterogeneous(t)) {
lean_trace_debug_ematch(tout() << "match_leaf with heq\n";);
buffer<state> new_states;
expr_set types_seen;
expr it = t;
do {
expr_set types_seen;
expr it_type = m_ctx->infer(it);
if (types_seen.find(it_type)) continue;
types_seen.insert(it_type);