feat(library/scoped_ext): do not import 'children' namespace objects

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/library/scoped_ext.h

@@ -65,13 +65,10 @@ class scoped_ext : public environment_extension {
     }
 
     void register_entry_core(name n, entry const & e) {
-        while (!n.is_anonymous()) {
-            if (auto it = m_entries.find(n))
-                m_entries.insert(n, list<entry>(e, *it));
-            else
-                m_entries.insert(n, list<entry>(e));
-            n = n.get_prefix();
-        }
+        if (auto it = m_entries.find(n))
+            m_entries.insert(n, list<entry>(e, *it));
+        else
+            m_entries.insert(n, list<entry>(e));
     }
 
     void add_entry_core(environment const & env, io_state const & ios, entry const & e) {

tests/lean/run/e13.lean

@@ -0,0 +1,26 @@
+precedence `+`:65
+
+namespace nat
+  variable nat : Type.{1}
+  variable add : nat → nat → nat
+  infixl + := add
+end
+
+namespace int
+  using nat (nat)
+  variable int : Type.{1}
+  variable add : int → int → int
+  infixl + := add
+  variable of_nat : nat → int
+  namespace coercions
+    coercion of_nat
+  end
+end
+
+using nat
+using int
+variables n m : nat
+check n+m -- coercion nat -> int is not available
+using int.coercions
+check n+m -- coercion nat -> int is available
+