From 1896e6e273605fbc5a7ebb9a50053d487d0a379d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 21 Oct 2014 14:50:50 -0700 Subject: [PATCH] feat(frontends/lean): allow 'reserve' inside namespaces --- src/frontends/lean/notation_cmd.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index f7cc6df3a..082fa143c 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -528,10 +528,7 @@ static environment prefix_cmd(parser & p) { static environment reserve_cmd(parser & p) { bool overload = false; bool reserve = true; - if (in_context(p.env()) || in_section(p.env()) || get_namespace(p.env())) { - throw parser_error("invalid reserve notation, command cannot be used in contexts/sections/namespaces", - p.pos()); - } else if (p.curr_is_token(get_notation_tk())) { + if (p.curr_is_token(get_notation_tk())) { p.next(); return notation_cmd_core(p, overload, reserve); } else if (p.curr_is_token(get_infixl_tk())) {