From 90ffb9d5ec61027c982a498a0fd15cfbedb8c5da Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 19 Jan 2014 19:47:40 -0800 Subject: [PATCH] fix(frontends/lean/pp): bug in pp_abstraction_core Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index d625cbf70..404f385fe 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -862,7 +862,8 @@ class pp_fn { \remark if T != 0, then T is Pi(x : A), B */ - result pp_abstraction_core(expr const & e, unsigned depth, optional T, std::vector const * implicit_args = nullptr) { + result pp_abstraction_core(expr const & e, unsigned depth, optional T, + std::vector const * implicit_args = nullptr) { local_names::mk_scope mk(m_local_names); if (is_arrow(e) && !implicit_args) { lean_assert(!T); @@ -889,7 +890,7 @@ class pp_fn { } format body_sep; if (T) { - format T_f = pp(*T, 0).first; + format T_f = pp_scoped_child(*T, 0).first; body_sep = format{space(), colon(), space(), T_f, space(), g_assign_fmt}; } else if (implicit_args) { // This is a little hack to pretty print Variable and