From 11860a65eb0bf4c7faf19bb53227db9a030b84cb Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 6 Feb 2019 14:24:37 +0100 Subject: [PATCH] fix(library/compiler/emit_cpp): replace constructor tag on `reuse` --- src/library/compiler/emit_cpp.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index a3bf77fb8b..d31896ecf7 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -477,6 +477,7 @@ struct emit_fn_fn { m_out << " "; emit_alloc_cnstr(x, cidx, args.size()-1, num_usizes, num_bytes); m_out << "} else {\n"; m_out << " "; emit_lhs(x); emit_fvar(o); m_out << ";\n"; + m_out << " lean::cnstr_set_tag("; emit_fvar(o); m_out << ", " << cidx << ");\n"; m_out << "}\n"; emit_cnstr_sets(x, args.size()-1, args.data()+1); }