max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/blast/blast): bug at visit_meta_app

Browse source
This commit is contained in:
Leonardo de Moura 2016-01-02 19:08:56 -08:00
parent 5feef27c2b
commit d85b4300b1
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/blast.cpp
View file

@ -400,7 +400,7 @@ class blastenv {
lean_assert(is_meta(aux));
expr type = visit(m_tc.infer(aux).first);
expr mref = m_state.mk_metavar(ctx, type);
m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(e, mref));
m_mvar2meta_mref.insert(mlocal_name(mvar), mk_pair(aux, mref));
return mk_mref_app(mref, args.size() - prefix_sz, args.data() + prefix_sz);
}
}