From 7342f342a92404914ee7e91d49b8ae3cf5f47810 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 28 May 2015 19:43:38 -0700
Subject: [PATCH] fix(frontends/lean/pp): fixes #634

---
 src/frontends/lean/pp.cpp        |  2 ++
 tests/lean/634.lean              | 17 +++++++++++++++++
 tests/lean/634.lean.expected.out |  5 +++++
 3 files changed, 24 insertions(+)
 create mode 100644 tests/lean/634.lean
 create mode 100644 tests/lean/634.lean.expected.out

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 6ecd1bb50..47c2550e1 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -377,6 +377,8 @@ auto pretty_fn::pp_child_core(expr const & e, unsigned bp, bool ignore_hide) ->
 // Return some result if \c e is of the form (c p_1 ... p_n) where
 // c is a constant, and p_i's are parameters fixed in a section.
 auto pretty_fn::pp_local_ref(expr const & e) -> optional<result> {
+    if (m_full_names)
+        return optional<result>();
     lean_assert(is_app(e));
     expr const & rfn = get_app_fn(e);
     if (is_constant(rfn)) {
diff --git a/tests/lean/634.lean b/tests/lean/634.lean
new file mode 100644
index 000000000..8c213d0e2
--- /dev/null
+++ b/tests/lean/634.lean
@@ -0,0 +1,17 @@
+open nat
+namespace foo
+section
+  parameter (X : Type₁)
+  definition A {n : ℕ} : Type₁ := X
+  variable {n : ℕ}
+  set_option pp.implicit true
+  check @A n
+  set_option pp.full_names true
+  check @foo.A X n
+  check @A n
+
+  set_option pp.full_names false
+  check @foo.A X n
+  check @A n
+end
+end foo
diff --git a/tests/lean/634.lean.expected.out b/tests/lean/634.lean.expected.out
new file mode 100644
index 000000000..99a07c0e0
--- /dev/null
+++ b/tests/lean/634.lean.expected.out
@@ -0,0 +1,5 @@
+A n : Type₁
+@foo.A X n : Type₁
+@foo.A X n : Type₁
+A n : Type₁
+A n : Type₁