From fe0b694a067d8377f5c320d8653efa01fe02130e Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 13 Apr 2017 18:15:34 -0700
Subject: [PATCH] feat(library/type_context): do not cache whnf in tmp_mode if
 term contains metavariables

---
 src/library/type_context.cpp | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 9f6b7f158f..a1756897ed 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -831,7 +831,8 @@ expr type_context::whnf(expr const & e) {
         if (auto next_t = unfold_definition(t1)) {
             t = *next_t;
         } else {
-            if (!m_used_assignment && !is_stuck(t1) &&
+            if ((!in_tmp_mode() || !has_expr_metavar(t1)) &&
+                !m_used_assignment && !is_stuck(t1) &&
                 postponed_sz == m_postponed.size() && !m_transparency_pred && !m_unfold_pred) {
                 cache.insert(mk_pair(e, t1));
             }