From caf28f4053412f6e7fdc984c382c34128a996fbe Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Apr 2015 21:08:57 -0700 Subject: [PATCH] fix(frontends/lean/decl_cmds): missing condition --- src/frontends/lean/decl_cmds.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 2555d661a..5c00834cf 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -172,9 +172,9 @@ optional parse_binder_info(parser & p, variable_kind k) { } static void check_variable_kind(parser & p, variable_kind k) { - if (in_context(p.env())) { + if (in_context(p.env()) || in_section(p.env())) { if (k == variable_kind::Axiom || k == variable_kind::Constant) - throw parser_error("invalid declaration, 'constant/axiom' cannot be used in contexts", + throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts", p.pos()); } else if (!in_section(p.env()) && !in_context(p.env()) && k == variable_kind::Parameter) { throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' "