diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp index 5e6973630a..282c19eeeb 100644 --- a/src/library/compiler/vm_compiler.cpp +++ b/src/library/compiler/vm_compiler.cpp @@ -315,7 +315,7 @@ public: } }; -environment vm_compile(environment const & env, buffer> const & procs) { +static environment vm_compile(environment const & env, buffer> const & procs) { environment new_env = env; for (auto const & p : procs) { new_env = reserve_vm_index(new_env, p.first, p.second); diff --git a/src/library/compiler/vm_compiler.h b/src/library/compiler/vm_compiler.h index 5750f9aef1..0d7cdbde7f 100644 --- a/src/library/compiler/vm_compiler.h +++ b/src/library/compiler/vm_compiler.h @@ -8,7 +8,6 @@ Author: Leonardo de Moura #include "kernel/environment.h" namespace lean { -environment vm_compile(environment const & env, buffer> const & procs); environment vm_compile(environment const & env, declaration const & d); void initialize_vm_compiler(); void finalize_vm_compiler();