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

chore(library/compiler/emit_bytecode): remove dead code

Browse source
This commit is contained in:
Leonardo de Moura 2018-11-01 14:21:20 -07:00
parent e5432f5fb2
commit f27ab2bb38
1 changed files with 0 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/library/compiler/emit_bytecode.cpp
View file

@ -186,14 +186,6 @@ class emit_bytecode_fn {
emit(mk_reuse_instr(cidx, get_app_num_args(e) - 1));
}
void compile_external(name const & n, buffer<expr> & args, unsigned bpz, vdecls const & m) {
// Not sure if this is the best approach, trying to lazy load the required
// dynamic libraries.
optional<vm_decl> decl = get_vm_decl(m_env, n);
lean_assert(decl);
compile_global(*decl, args.size(), args.data(), bpz, m);
}
void compile_fn_call(expr const & e, unsigned bpz, vdecls const & m) {
buffer<expr> args;
expr fn = get_app_args(e, args);