From 382d4d32b7f56385711af832eefd3601e5777051 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 14 Jun 2015 15:48:36 -0700 Subject: [PATCH] feat(frontends/lean): 'override' command and '# ' notation also override aliases Before this commit they were only overriding notation declarations. --- src/frontends/lean/builtin_cmds.cpp | 1 + src/frontends/lean/builtin_exprs.cpp | 1 + 2 files changed, 2 insertions(+) diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp index 672c106c5..0797e2f56 100644 --- a/src/frontends/lean/builtin_cmds.cpp +++ b/src/frontends/lean/builtin_cmds.cpp @@ -849,6 +849,7 @@ static environment override_cmd(parser & p) { ns = *real_ns; bool persistent = false; env = override_notation(env, ns, persistent); + env = overwrite_aliases(env, ns, name()); env = update_fingerprint(env, ns.hash()); } return env; diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp index 723e2c7aa..5c1fcb78a 100644 --- a/src/frontends/lean/builtin_exprs.cpp +++ b/src/frontends/lean/builtin_exprs.cpp @@ -564,6 +564,7 @@ static expr parse_override_notation(parser & p, unsigned, expr const *, pos_info name n = p.check_id_next("invalid '#' local notation, identifier expected"); bool persistent = false; environment env = override_notation(p.env(), n, persistent); + env = overwrite_aliases(env, n, name()); return p.parse_expr_with_env(env); }