From e5182fe4af238f9a56a23de49714f5087164f90e Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Fri, 28 May 2021 15:48:41 -0700
Subject: [PATCH] fix: exported symbol arities

---
 src/kernel/local_ctx.cpp | 4 ++--
 src/runtime/io.cpp       | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp
index 10c651c7d6..8849505dec 100644
--- a/src/kernel/local_ctx.cpp
+++ b/src/kernel/local_ctx.cpp
@@ -45,7 +45,7 @@ extern "C" object * lean_mk_empty_local_ctx(object*);
 extern "C" object * lean_local_ctx_num_indices(object*);
 extern "C" uint8 lean_local_ctx_is_empty(object*);
 extern "C" object * lean_local_ctx_mk_local_decl(object * lctx, object * name, object * user_name, object * expr, uint8 bi);
-extern "C" object * lean_local_ctx_mk_let_decl(object * lctx, object * name, object * user_name, object * type, object * value);
+extern "C" object * lean_local_ctx_mk_let_decl(object * lctx, object * name, object * user_name, object * type, object * value, uint8 non_dep);
 extern "C" object * lean_local_ctx_find(object * lctx, object * name);
 extern "C" object * lean_local_ctx_erase(object * lctx, object * name);
 
@@ -58,7 +58,7 @@ bool local_ctx::empty() const {
 
 local_decl local_ctx::mk_local_decl(name const & n, name const & un, expr const & type, expr const & value) {
     unsigned idx = unbox(lean_local_ctx_num_indices(to_obj_arg()));
-    m_obj = lean_local_ctx_mk_let_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg());
+    m_obj = lean_local_ctx_mk_let_decl(raw(), n.to_obj_arg(), un.to_obj_arg(), type.to_obj_arg(), value.to_obj_arg(), false);
     return local_decl(idx, n, un, type, value);
 }
 
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 18c1981d39..9b1a76230c 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -736,7 +736,7 @@ extern "C" obj_res lean_io_wait(obj_arg t, obj_arg) {
     return io_result_mk_ok(lean_task_get_own(t));
 }
 
-extern "C" obj_res lean_io_wait_any(b_obj_arg task_list) {
+extern "C" obj_res lean_io_wait_any(b_obj_arg task_list, obj_arg) {
     object * t = lean_io_wait_any_core(task_list);
     object * v = lean_task_get(t);
     lean_inc(v);