max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/type_context): fix tmp_mode assertion error

Browse source 
Fixes #1543
This commit is contained in:
Sebastian Ullrich 2017-04-26 19:58:49 +02:00 • committed by Leonardo de Moura
parent cfbc449769
commit 8cf98d9974
1 changed files with 2 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/library/type_context.cpp
View file

@ -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