diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index e59ebebe9f..6d3fcb7c10 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -55,6 +55,8 @@ class vm_compiler_fn {
         if (decl.get_arity() <= nargs) {
             if (decl.is_builtin())
                 emit(mk_invoke_builtin_instr(decl.get_idx()));
+            else if (decl.is_cfun())
+                emit(mk_invoke_cfun_instr(decl.get_idx()));
             else
                 emit(mk_invoke_global_instr(decl.get_idx()));
             emit_apply_instr(nargs - decl.get_arity());
diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp
index bad6bb397f..b6175bb57d 100644
--- a/src/library/vm/vm.cpp
+++ b/src/library/vm/vm.cpp
@@ -575,6 +575,7 @@ void vm_decl_cell::dealloc() {
 
 /** \brief VM builtin functions */
 static name_map<pair<unsigned, vm_function>> * g_vm_builtins = nullptr;
+static name_map<pair<unsigned, vm_cfunction>> * g_vm_cbuiltins = nullptr;
 static bool g_may_update_vm_builtins = true;
 
 void declare_vm_builtin(name const & n, unsigned arity, vm_function fn) {
@@ -582,8 +583,53 @@ void declare_vm_builtin(name const & n, unsigned arity, vm_function fn) {
     g_vm_builtins->insert(n, mk_pair(arity, fn));
 }
 
+void declare_vm_builtin(name const & n, vm_cfunction_1 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(1, fn));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_2 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(2, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_3 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(3, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_4 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(4, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_5 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(5, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_6 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(6, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_7 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(7, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, vm_cfunction_8 fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(8, reinterpret_cast<vm_cfunction>(fn)));
+}
+
+void declare_vm_builtin(name const & n, unsigned arity, vm_cfunction_N fn) {
+    lean_assert(g_may_update_vm_builtins);
+    g_vm_cbuiltins->insert(n, mk_pair(arity, reinterpret_cast<vm_cfunction>(fn)));
+}
+
 bool is_vm_builtin_function(name const & fn) {
-    return g_vm_builtins->contains(fn);
+    return g_vm_builtins->contains(fn) || g_vm_cbuiltins->contains(fn);
 }
 
 /** \brief VM function/constant declarations are stored in an environment extension. */
@@ -595,6 +641,9 @@ struct vm_decls : public environment_extension {
         g_vm_builtins->for_each([&](name const & n, pair<unsigned, vm_function> const & p) {
                 add(vm_decl(n, m_decls.size(), p.first, p.second));
             });
+        g_vm_cbuiltins->for_each([&](name const & n, pair<unsigned, vm_cfunction> const & p) {
+                add(vm_decl(n, m_decls.size(), p.first, p.second));
+            });
     }
 
     void add(vm_decl const & d) {
@@ -1810,6 +1859,7 @@ void display_vm_code(std::ostream & out, environment const & env, unsigned code_
 
 void initialize_vm_core() {
     g_vm_builtins = new name_map<pair<unsigned, vm_function>>();
+    g_vm_cbuiltins = new name_map<pair<unsigned, vm_cfunction>>();
     g_may_update_vm_builtins = true;
     DEBUG_CODE({
             /* We only trace VM in debug mode because it produces a 10% performance penalty */
@@ -1820,6 +1870,7 @@ void initialize_vm_core() {
 
 void finalize_vm_core() {
     delete g_vm_builtins;
+    delete g_vm_cbuiltins;
 }
 
 void initialize_vm() {
diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h
index 98a14c607f..67bb37cac9 100644
--- a/src/library/vm/vm.h
+++ b/src/library/vm/vm.h
@@ -530,8 +530,18 @@ public:
     vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
 };
 
-/** \brief Add builtin implementation for the function named \c n. */
+/** \brief Add builtin implementation for the function named \c n.
+    All environment objects will contain this builtin. */
 void declare_vm_builtin(name const & n, unsigned arity, vm_function fn);
+void declare_vm_builtin(name const & n, vm_cfunction_1 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_2 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_3 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_4 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_5 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_6 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_7 fn);
+void declare_vm_builtin(name const & n, vm_cfunction_8 fn);
+void declare_vm_builtin(name const & n, unsigned arity, vm_cfunction_N fn);
 
 /** \brief Reserve an index for the given function in the VM, the expression
     \c e is the value of \c fn after preprocessing.