diff --git a/tests/lean/run/section2.lean b/tests/lean/run/section2.lean
new file mode 100644
index 000000000..3a637d538
--- /dev/null
+++ b/tests/lean/run/section2.lean
@@ -0,0 +1,17 @@
+import data.nat
+
+section foo
+  parameter A : Type
+  definition id (a : A) := a
+  variable a : nat
+  check _root_.id nat a
+end foo
+
+namespace n1
+section foo
+  parameter A : Type
+  definition id (a : A) := a
+  variable a : nat
+  check n1.id _ a
+end foo
+end n1