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

fix(library/type_context): instantiate was not replacing all assigned metavars

Browse source
This commit is contained in:
Leonardo de Moura 2016-03-23 13:37:33 -07:00
parent 1c52062f1e
commit 6f74f65220
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/type_context.cpp
View file

@ -590,7 +590,7 @@ struct instantiate_uvars_mvars_fn : public replace_visitor {
virtual expr visit_meta(expr const & m) override {
if (m_owner.is_mvar(m)) {
if (auto v1 = m_owner.get_assignment(m)) {
if (!has_expr_metavar(*v1)) {
if (!has_metavar(*v1)) {
return *v1;
} else {
expr v2 = m_owner.instantiate_uvars_mvars(*v1);