fix(frontends/lean/pp): fixes #634

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)) {

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

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₁