From 6950b4aa9b416dcfe02fd929806439cac0c9ecbb Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 2 Oct 2014 18:29:41 -0700
Subject: [PATCH] fix(frontends/lean/decl_cmds): do not allow section
 parameters/variables to shadow existing parameters/variables

---
 src/frontends/lean/decl_cmds.cpp |  2 ++
 tests/lean/sec.lean              | 11 +++++++++++
 tests/lean/sec.lean.expected.out |  1 +
 3 files changed, 14 insertions(+)
 create mode 100644 tests/lean/sec.lean
 create mode 100644 tests/lean/sec.lean.expected.out

diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 3b5715b55..e03622b1c 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -85,6 +85,8 @@ static environment declare_var(parser & p, environment env,
         lean_assert(k == variable_kind::Parameter || k == variable_kind::Variable);
         if (k == variable_kind::Parameter)
             check_parameter_type(p, n, type, pos);
+        if (p.get_local(n))
+            throw parser_error(sstream() << "invalid declaration, section/context already contains '" << n << "'", pos);
         name u = p.mk_fresh_name();
         expr l = p.save_pos(mk_local(u, n, type, bi), pos);
         p.add_local_expr(n, l, k == variable_kind::Variable);
diff --git a/tests/lean/sec.lean b/tests/lean/sec.lean
new file mode 100644
index 000000000..ec306d76e
--- /dev/null
+++ b/tests/lean/sec.lean
@@ -0,0 +1,11 @@
+import data.prod
+open prod
+
+section
+  variable A : Type
+  variable a : A
+  variable A : Type
+  variable b : A
+
+  definition foo := a
+end
diff --git a/tests/lean/sec.lean.expected.out b/tests/lean/sec.lean.expected.out
new file mode 100644
index 000000000..5c89956cc
--- /dev/null
+++ b/tests/lean/sec.lean.expected.out
@@ -0,0 +1 @@
+sec.lean:7:11: error: invalid declaration, section/context already contains 'A'