From 6060b75e628e149fe0b3c39bf1acac09610f1538 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 1 Feb 2018 17:46:31 -0800 Subject: [PATCH] fix(library/local_context): propagate m_instance_fingerprint --- src/library/local_context.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index d83a5778ea..5461a738f2 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -459,7 +459,8 @@ name local_context::get_unused_name(name const & suggestion) const { local_context local_context::instantiate_mvars(metavar_context & mctx) const { local_context r; - r.m_next_idx = m_next_idx; + r.m_next_idx = m_next_idx; + r.m_instance_fingerprint = m_instance_fingerprint; m_idx2local_decl.for_each([&](unsigned, local_decl const & d) { expr new_type = mctx.instantiate_mvars(d.m_ptr->m_type); optional new_value;