From da785d96a0c03308210520a69e4f87cdb334fd2b Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 1 Sep 2017 14:24:11 +0200 Subject: [PATCH] fix(frontends/lean/elaborator): synthesize metavars in `e` before trying to synthesize `reflected e` --- src/frontends/lean/elaborator.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 8835008aa4..3c5edc1aed 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3196,6 +3196,7 @@ expr elaborator::visit_expr_quote(expr const & e, optional const & expecte } else { new_s = visit(s, none_expr()); } + synthesize(); // try to instantiate all metavars in `new_s`, otherwise reflection will fail expr cls = mk_app(m_ctx, get_reflected_name(), new_s); return mk_instance(cls, e); }