diff --git a/src/frontends/lean/builtin_cmds.cpp b/src/frontends/lean/builtin_cmds.cpp
index 908f88103..4771179ef 100644
--- a/src/frontends/lean/builtin_cmds.cpp
+++ b/src/frontends/lean/builtin_cmds.cpp
@@ -274,7 +274,7 @@ static void redeclare_aliases(parser & p,
                               list<pair<name, level>> old_level_entries,
                               list<pair<name, expr>> old_entries) {
     environment const & env = p.env();
-    if (!in_context(env))
+    if (!in_context(env) && !in_section(env))
         return;
     list<pair<name, expr>> new_entries = p.get_local_entries();
     buffer<pair<name, expr>> to_redeclare;
diff --git a/tests/lean/run/section4.lean b/tests/lean/run/section4.lean
index f70eb4a3b..5a4f427de 100644
--- a/tests/lean/run/section4.lean
+++ b/tests/lean/run/section4.lean
@@ -7,7 +7,7 @@ section
   universe k
   parameter A : Type
 
-  context
+  section
     universe variable l
     universe variable u
     parameter B : Type