From 8cf98d99741ff13e87be863a909796bb3bba51b8 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 26 Apr 2017 19:58:49 +0200
Subject: [PATCH] fix(library/type_context): fix tmp_mode assertion error

Fixes #1543
---
 src/library/type_context.cpp | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 901894ae7b..8eeef37e93 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -3497,6 +3497,7 @@ struct instance_synthesizer {
                 }
             }
             lean_trace("class_instances",
+                       scope_trace_env scope(m_ctx.env(), m_ctx);
                        tout() << "trying next solution, current solution has metavars\n" << *r << "\n";);
             r = next_solution();
         }
@@ -3510,6 +3511,7 @@ struct instance_synthesizer {
             if (it != m_ctx.m_cache->m_instance_cache.end()) {
                 /* instance/failure is already cached */
                 lean_trace("class_instances",
+                           scope_trace_env scope(m_ctx.env(), m_ctx);
                            if (it->second)
                                tout() << "cached instance for " << type << "\n" << *(it->second) << "\n";
                            else