From 60ff0571599abcdeea0539da2266e41b89d3ecdd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 May 2015 15:09:31 -0700
Subject: [PATCH] test(tests/lean): add missing test for issue #634

---
 tests/lean/634d.lean              | 24 ++++++++++++++++++++++++
 tests/lean/634d.lean.expected.out | 10 ++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 tests/lean/634d.lean
 create mode 100644 tests/lean/634d.lean.expected.out

diff --git a/tests/lean/634d.lean b/tests/lean/634d.lean
new file mode 100644
index 000000000..9223d3547
--- /dev/null
+++ b/tests/lean/634d.lean
@@ -0,0 +1,24 @@
+open nat
+section
+  universe l
+  definition A {n : ℕ} (t : Type.{l}) := t
+  check A
+  check _root_.A.{1}
+  set_option pp.universes true
+  check A
+  check _root_.A.{1}
+end
+
+section
+  universe l
+  parameters {B : Type.{l}}
+  definition P {n : ℕ} (b : B) := b
+  check P
+  check @_root_.P.{1} nat
+  set_option pp.universes true
+  check P
+  check _root_.P.{1}
+  set_option pp.implicit true
+  check @P 2
+  check @_root_.P.{1} nat
+end
diff --git a/tests/lean/634d.lean.expected.out b/tests/lean/634d.lean.expected.out
new file mode 100644
index 000000000..d18dece02
--- /dev/null
+++ b/tests/lean/634d.lean.expected.out
@@ -0,0 +1,10 @@
+A : Type → Type
+_root_.A : Type₁ → Type₁
+A : Type.{l} → Type.{l}
+_root_.A.{1} : Type₁ → Type₁
+P : B → B
+_root_.P.{1} : Π {n : ℕ}, ℕ → ℕ
+P : B → B
+_root_.P.{1} : ?B → ?B
+@P 2 : B → B
+@_root_.P.{1} ℕ : Π {n : ℕ}, ℕ → ℕ