From d10bb92a7d6c9c35418d9799617cc622ebe12e34 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Dec 2014 14:25:02 -0800
Subject: [PATCH] feat(library/aliases): protected definitions in nested
 namespaces, closes #331

---
 src/library/aliases.cpp | 12 ++++++------
 tests/lean/run/331.lean | 21 +++++++++++++++++++++
 2 files changed, 27 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/331.lean

diff --git a/src/library/aliases.cpp b/src/library/aliases.cpp
index 26fa44a57..e5e897c3e 100644
--- a/src/library/aliases.cpp
+++ b/src/library/aliases.cpp
@@ -190,20 +190,20 @@ environment add_aliases(environment const & env, name const & prefix, name const
                         unsigned num_exceptions, name const * exceptions, bool overwrite) {
     aliases_ext ext = get_extension(env);
     env.for_each_declaration([&](declaration const & d) {
-            if (!is_protected(env, d.get_name()) &&
-                is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
+            if (is_prefix_of(prefix, d.get_name()) && !is_exception(d.get_name(), prefix, num_exceptions, exceptions)) {
                 name a        = d.get_name().replace_prefix(prefix, new_prefix);
-                if (!a.is_anonymous())
+                if (!(is_protected(env, d.get_name()) && a.is_atomic()) &&
+                    !(a.is_anonymous()))
                     ext.add_expr_alias(a, d.get_name(), overwrite);
             }
         });
     env.for_each_universe([&](name const & u) {
-            if (!is_protected(env, u) &&
-                is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
+            if (is_prefix_of(prefix, u) && !is_exception(u, prefix, num_exceptions, exceptions)) {
                 name a = u.replace_prefix(prefix, new_prefix);
                 if (env.is_universe(a))
                     throw exception(sstream() << "universe level alias '" << a << "' shadows existing global universe level");
-                if (!a.is_anonymous())
+                if (!(is_protected(env, u) && a.is_atomic()) &&
+                    !a.is_anonymous())
                     ext.add_level_alias(a, u);
             }
         });
diff --git a/tests/lean/run/331.lean b/tests/lean/run/331.lean
new file mode 100644
index 000000000..ad3188d6e
--- /dev/null
+++ b/tests/lean/run/331.lean
@@ -0,0 +1,21 @@
+namespace nat
+  inductive less (a : nat) : nat → Prop :=
+  base : less a (succ a),
+  step : Π {b}, less a b → less a (succ b)
+
+end nat
+
+open nat
+check less.rec_on
+
+namespace foo1
+protected definition foo2.bar := 10
+end foo1
+
+example : foo1.foo2.bar = 10 :=
+rfl
+
+open foo1
+
+example : foo2.bar = 10 :=
+rfl