From 3615073faf9e04eced17f8fdee641c88532ae7ee Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 May 2018 16:21:52 -0700 Subject: [PATCH] fix(frontends/lean/elaborator): visit_expr_quote bug --- src/frontends/lean/elaborator.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp index 242f7120ac..653a7a8ca8 100644 --- a/src/frontends/lean/elaborator.cpp +++ b/src/frontends/lean/elaborator.cpp @@ -3316,6 +3316,8 @@ expr elaborator::visit_expr_quote(expr const & e, optional const & expecte }); s = Fun(locals, s); expr new_s = visit(s, none_expr()); + synthesize(); + new_s = instantiate_mvars(new_s); if (has_param_univ(new_s)) throw elaborator_exception(e, "invalid quotation, contains universe parameter"); if (has_univ_metavar(new_s))