michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(frontends/lean/decl_cmds): error messages

Browse source
This commit is contained in:
Leonardo de Moura 2014-10-13 07:17:33 -07:00
parent 08c0fb3a64
commit 698dc0472d
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/frontends/lean/decl_cmds.cpp
View file

@ -155,12 +155,12 @@ optional<binder_info> parse_binder_info(parser & p, variable_kind k) {
static void check_variable_kind(parser & p, variable_kind k) {
if (in_context(p.env())) {
if (k == variable_kind::Axiom || k == variable_kind::Constant)
throw parser_error("invalid declaration, 'constant/axiom' cannot be used in sections/contexts",
throw parser_error("invalid declaration, 'constant/axiom' cannot be used in contexts",
p.pos());
} else {
if (k == variable_kind::Parameter)
throw parser_error("invalid declaration, 'parameter/hypothesis/conjecture' "
"can only be used in sections/contexts", p.pos());
"can only be used in contexts", p.pos());
}
}