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

refactor(library/aliases): cleanup

Browse source
This commit is contained in:
Leonardo de Moura 2015-08-11 06:40:45 -07:00
parent a5615a6ea7
commit 23118371d1
2 changed files with 7 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/frontends/lean/parser.cpp
View file

@ -741,6 +741,13 @@ level parser::parse_level_id() {
next(); next();
if (auto it = m_local_level_decls.find(id)) if (auto it = m_local_level_decls.find(id))
return *it; return *it;
for (name const & ns : get_namespaces(m_env)) {
auto new_id = ns + id;
if (!ns.is_anonymous() && m_env.is_universe(new_id))
return mk_global_univ(new_id);
}
if (m_env.is_universe(id)) if (m_env.is_universe(id))
return mk_global_univ(id); return mk_global_univ(id);
if (auto it = get_level_alias(m_env, id)) if (auto it = get_level_alias(m_env, id))

2
src/library/aliases.cpp
View file

@ -106,8 +106,6 @@ struct aliases_ext : public environment_extension {
aliases_ext ext = get_extension(env); aliases_ext ext = get_extension(env);
ext.push(k != scope_kind::Namespace); ext.push(k != scope_kind::Namespace);
environment new_env = update(env, ext); environment new_env = update(env, ext);
if (!::lean::in_section(new_env))
new_env = add_aliases(new_env, get_namespace(new_env), name());
return new_env; return new_env;
} }