From 94be486aded19fbd0b9155afbbc45068834188ed Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 7 May 2016 18:39:40 -0700 Subject: [PATCH] fix(frontends/lean/builtin_cmds): generate error if declaration is not a definition --- src/frontends/lean/builtin_cmds.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 2d387f2508..696101eab9 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -654,8 +654,11 @@ static environment abstract_expr_cmd(parser & p) { } static environment compile_cmd(parser & p) { + auto pos = p.pos(); name n = p.check_constant_next("invalid #compile command, constant expected"); declaration d = p.env().get(n); + if (!d.is_definition()) + throw parser_error("invalid #compile command, declaration is not a definition", pos); buffer> procs; preprocess_rec(p.env(), d, procs); return p.env();