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

fix(library/compiler/emit_cpp): replace constructor tag on reuse

Browse source
This commit is contained in:
Sebastian Ullrich 2019-02-06 14:24:37 +01:00 • committed by Leonardo de Moura
parent eb85081a03
commit 11860a65eb
1 changed files with 1 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/library/compiler/emit_cpp.cpp
View file

@ -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);
}