diff --git a/src/Init/Lean/Compiler/IR/CtorLayout.lean b/src/Init/Lean/Compiler/IR/CtorLayout.lean index 892dc2fad8..e3fe13f61a 100644 --- a/src/Init/Lean/Compiler/IR/CtorLayout.lean +++ b/src/Init/Lean/Compiler/IR/CtorLayout.lean @@ -36,7 +36,7 @@ structure CtorLayout := (scalarSize : Nat) @[extern "lean_ir_get_ctor_layout"] -constant getCtorLayout (env : Environment) (ctorName : Name) : Except String CtorLayout := arbitrary _ +constant getCtorLayout (env : @& Environment) (ctorName : @& Name) : Except String CtorLayout := arbitrary _ end IR end Lean diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index 3f62ff6136..43246de9c8 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/src/library/compiler/ir_interpreter.cpp @@ -838,8 +838,8 @@ public: for (unsigned i = 0; i < arity; i++) { m_arg_stack.push_back(args[i]); } - push_frame(e.m_decl, 0); - r = eval_body(decl_fun_body(e.m_decl)).m_obj; + push_frame(d, 0); + r = eval_body(decl_fun_body(d)).m_obj; if (n > arity) { // `fn` returned a closure r = apply_n(r, n - arity, &args[arity]);