From 1cee5fbfea019c6ea3970f40de69de535002575c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 5 Nov 2016 14:11:21 -0700
Subject: [PATCH] chore(library/compiler/vm_compiler): hide API

---
 src/library/compiler/vm_compiler.cpp | 2 +-
 src/library/compiler/vm_compiler.h   | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

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<pair<name, expr>> const & procs) {
+static environment vm_compile(environment const & env, buffer<pair<name, expr>> 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<pair<name, expr>> const & procs);
 environment vm_compile(environment const & env, declaration const & d);
 void initialize_vm_compiler();
 void finalize_vm_compiler();