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 : ℕ}, ℕ → ℕ