From 23118371d1e89594656c840e6919aab832ead602 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 11 Aug 2015 06:40:45 -0700
Subject: [PATCH] refactor(library/aliases): cleanup

---
 src/frontends/lean/parser.cpp | 7 +++++++
 src/library/aliases.cpp       | 2 --
 2 files changed, 7 insertions(+), 2 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 39300669d..b53590ec7 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -741,6 +741,13 @@ level parser::parse_level_id() {
     next();
     if (auto it = m_local_level_decls.find(id))
         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))
         return mk_global_univ(id);
     if (auto it = get_level_alias(m_env, id))
diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 18165aee7..0c449e47f 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -106,8 +106,6 @@ struct aliases_ext : public environment_extension {
         aliases_ext ext = get_extension(env);
         ext.push(k != scope_kind::Namespace);
         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;
     }