From 0ccac266be0d6c35bc45f014ee582942fc622e38 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 10 Jun 2016 14:52:33 -0700 Subject: [PATCH] fix(library/type_context): use get_pp_name --- src/library/type_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index 4aba9e3856..e1f16e9911 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -210,7 +210,7 @@ type_context::~type_context() { name type_context::get_local_pp_name(expr const & e) const { lean_assert(is_local(e)); if (is_local_decl_ref(e)) - return m_lctx.get_local_decl(e)->get_name(); + return m_lctx.get_local_decl(e)->get_pp_name(); else return local_pp_name(e); }