From f820f3f97e9b5dbee51af512a799bac337a543b2 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 31 May 2017 16:05:47 +0200 Subject: [PATCH] fix(frontends/lean/builtin_cmds): abort `eval` after error recovery and complain about unsynthesized mvars early --- src/frontends/lean/builtin_cmds.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index c9c737be2f..0523a3a477 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -432,9 +432,9 @@ static environment compile_cmd(parser & p) { static environment eval_cmd(parser & p) { auto pos = p.pos(); expr e; level_param_names ls; - std::tie(e, ls) = parse_local_expr(p, "_eval"); - if (has_metavar(e)) - throw parser_error("invalid eval command, expression contains metavariables", pos); + std::tie(e, ls) = parse_local_expr(p, "_eval", /* relaxed */ false); + if (has_synthetic_sorry(e)) + return p.env(); type_context tc(p.env(), transparency_mode::All); auto type = tc.infer(e);