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

fix(library/compiler/emit_cpp): remove leftover

Browse source
This commit is contained in:
Leonardo de Moura 2019-02-01 14:21:17 -08:00
parent 42ee42b732
commit b6f7472dd7
1 changed files with 0 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -485,7 +485,6 @@ struct emit_fn_fn {
void emit_uset(expr const & x, expr const & fn, buffer<expr> const & args) {
unsigned n;
lean_verify(is_llnf_uset(fn, n));
emit_lhs(x);
m_out << "lean::cnstr_set_scalar("; emit_fvar(args[0]); m_out << ", "; emit_offset(n, 0); m_out << ", "; emit_fvar(args[1]); m_out << ");\n";
emit_lhs(x); emit_fvar(args[0]); m_out << ";\n";
}