From cdc0a5ac2900738faa61b63b3a0bc055d132035d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 29 Sep 2018 17:13:55 -0700 Subject: [PATCH] fix(library/compiler/vm_compiler): add support for kernel projections --- src/library/compiler/vm_compiler.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 804d4105fc..891c5a3d6f 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -283,8 +283,9 @@ class vm_compiler_fn { } } - void compile_proj_cnstr(expr const & /* e */, unsigned /* bpz */, name_map const & /* m */) { - lean_unreachable(); + void compile_proj_cnstr(expr const & e, unsigned bpz, name_map const & m) { + compile(proj_expr(e), bpz, m); + emit(mk_proj_instr(proj_idx(e).get_small_value())); } void compile(expr const & e, unsigned bpz, name_map const & m) {