From c2959dc77b3e3bbb468ea50ca76db53a1d1e6a6b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 13 May 2016 16:26:34 -0700 Subject: [PATCH] feat(frontends/lean/builtin_cmds): improve error message --- src/frontends/lean/builtin_cmds.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index fa309f5cb7..be039a002f 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -665,11 +665,8 @@ static environment compile_cmd(parser & p) { } static environment vm_eval_cmd(parser & p) { - auto pos = p.pos(); expr e; level_param_names ls; std::tie(e, ls) = parse_local_expr(p); - if (has_local(e) || has_metavar(e)) - throw parser_error("invalid vm_eval command, argument must be a closed expression", pos); type_checker tc(p.env()); expr type = tc.infer(e); environment new_env = p.env();