From 73eca1ef44ba52de3b784aa4d22b56d5ae37a7f6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 3 Oct 2014 12:51:29 -0700 Subject: [PATCH] feat(frontends/lean/notation_cmd): notation defined in context overrides existing ones --- src/frontends/lean/notation_cmd.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/frontends/lean/notation_cmd.cpp b/src/frontends/lean/notation_cmd.cpp index 2a2ccc60b..87c5e2b1a 100644 --- a/src/frontends/lean/notation_cmd.cpp +++ b/src/frontends/lean/notation_cmd.cpp @@ -420,11 +420,11 @@ notation_entry parse_notation(parser & p, bool overload, buffer & n } } -environment notation_cmd(parser & p) { return notation_cmd_core(p, true); } -environment infixl_cmd(parser & p) { return infixl_cmd_core(p, true); } -environment infixr_cmd(parser & p) { return infixr_cmd_core(p, true); } -environment postfix_cmd(parser & p) { return postfix_cmd_core(p, true); } -environment prefix_cmd(parser & p) { return prefix_cmd_core(p, true); } +environment notation_cmd(parser & p) { return notation_cmd_core(p, !in_context(p.env())); } +environment infixl_cmd(parser & p) { return infixl_cmd_core(p, !in_context(p.env())); } +environment infixr_cmd(parser & p) { return infixr_cmd_core(p, !in_context(p.env())); } +environment postfix_cmd(parser & p) { return postfix_cmd_core(p, !in_context(p.env())); } +environment prefix_cmd(parser & p) { return prefix_cmd_core(p, !in_context(p.env())); } void register_notation_cmds(cmd_table & r) { add_cmd(r, cmd_info("precedence", "set token left binding power", precedence_cmd));