From d85b4300b16c2c44bac2febca3feeaab0e6bb198 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 2 Jan 2016 19:08:56 -0800 Subject: [PATCH] fix(library/blast/blast): bug at visit_meta_app --- src/library/blast/blast.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index ecec827b1f..db2e03bc52 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -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); } }