From 4528711efbbc4f5629f31f553362749a13f83044 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 18 May 2017 07:26:16 +0200
Subject: [PATCH] fix(library/type_context): prevent segfault

Temporary metavariables appeared here when pretty-printing simp_lemmas.
---
 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 adc7e3f95c..9275166e11 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -797,7 +797,7 @@ expr type_context::whnf_core(expr const & e, bool proj_reduce) {
                 m_used_assignment = true;
                 return whnf_core(m_mctx.instantiate_mvars(e), proj_reduce);
             }
-        } else if (is_idx_metavar(e)) {
+        } else if (m_tmp_data && is_idx_metavar(e)) {
             lean_assert(in_tmp_mode());
             unsigned idx = to_meta_idx(e);
             if (idx < m_tmp_data->m_eassignment.size()) {