From 695bba629184da8484b07e24d882ffcea5455b2e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 13 Jun 2016 12:26:03 -0700 Subject: [PATCH] fix(library/type_context): make sure code doesn't fail if local decl does not exist --- src/library/type_context.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp index e1f16e9911..01412358e1 100644 --- a/src/library/type_context.cpp +++ b/src/library/type_context.cpp @@ -209,10 +209,11 @@ 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_pp_name(); - else - return local_pp_name(e); + if (is_local_decl_ref(e)) { + if (auto d = m_lctx.get_local_decl(e)) + return d->get_pp_name(); + } + return local_pp_name(e); } expr type_context::push_local(name const & pp_name, expr const & type, binder_info const & bi) {