From 2631979f5c15a8200fff0b0c2fde85c3abfacc2a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 7 Sep 2014 19:55:19 -0700
Subject: [PATCH] fix(library/scoped_ext): section/context should not affect
 namespace

---
 src/library/scoped_ext.cpp  | 4 +++-
 tests/lean/run/sec_bug.lean | 9 +++++++++
 2 files changed, 12 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/run/sec_bug.lean

diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 30a532c28..fc787182a 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -99,7 +99,9 @@ static std::string g_new_namespace_key("nspace");
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
     if (k == scope_kind::Namespace && in_section_or_context(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
-    name new_n = get_namespace(env) + n;
+    name new_n = get_namespace(env);
+    if (k == scope_kind::Namespace)
+        new_n = new_n + n;
     scope_mng_ext ext = get_extension(env);
     bool save_ns = false;
     if (!ext.m_namespace_set.contains(new_n)) {
diff --git a/tests/lean/run/sec_bug.lean b/tests/lean/run/sec_bug.lean
new file mode 100644
index 000000000..c7500b97d
--- /dev/null
+++ b/tests/lean/run/sec_bug.lean
@@ -0,0 +1,9 @@
+import logic
+
+namespace foo
+section bla
+  definition tst := true
+end bla
+end foo
+
+check foo.tst