From fe9f4dd95f2c8888579d36c35cc2c7663c802cb0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 21 Apr 2015 19:50:21 -0700
Subject: [PATCH] fix(frontends/lean): another bug in sections with parameters

---
 src/frontends/lean/builtin_cmds.cpp | 2 +-
 tests/lean/run/section4.lean        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

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