From d01e2d7ae8250e8f69139d8cb37950079e76ca9d Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Thu, 1 Feb 2018 16:04:04 +0000
Subject: [PATCH] fix(msvc): change previous MSVC workaround to change the code
 less

---
 src/library/compiler/vm_compiler.cpp            | 4 ++--
 src/library/native_compiler/native_compiler.cpp | 8 ++++----
 src/library/native_compiler/used_defs.cpp       | 4 ++--
 src/library/native_compiler/used_defs.h         | 4 ++--
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/library/compiler/vm_compiler.cpp b/src/library/compiler/vm_compiler.cpp
index a68146fc21..1861f0eebe 100644
--- a/src/library/compiler/vm_compiler.cpp
+++ b/src/library/compiler/vm_compiler.cpp
@@ -344,9 +344,9 @@ public:
 };
 
 buffer<name> extern_names(environment const & env, buffer<procedure> const & procs) {
-    used_defs live_names(env, [&] (used_defs & live_names, declaration const & d) {
+    used_defs live_names{env, [&] (declaration const & d) {
         live_names.names_in_decl(d);
-    });
+    }};
 
     for (auto p : procs) {
         live_names.names_in_preprocessed_body(p.m_code);
diff --git a/src/library/native_compiler/native_compiler.cpp b/src/library/native_compiler/native_compiler.cpp
index 700df174bf..7deab90331 100644
--- a/src/library/native_compiler/native_compiler.cpp
+++ b/src/library/native_compiler/native_compiler.cpp
@@ -359,7 +359,7 @@ void native_compile_module(environment const & env, buffer<declaration> decls) {
 
     // Compute the live set of names, we attach a callback that will be
     // invoked for every declaration encountered.
-    used_defs used_names(env, [&] (used_defs & used_names, declaration const & d) {
+    used_defs used_names{env, [&] (declaration const & d) {
         buffer<procedure> procs;
         // The the name is an internal decl we should not add it to the live set.
         if (is_internal_decl(d)) {
@@ -379,7 +379,7 @@ void native_compile_module(environment const & env, buffer<declaration> decls) {
                 all_procs.push_back(pair);
             }
         }
-    });
+    }};
 
     // We then loop over the set of procs produced by preprocessing the
     // main function, we transitively collect all names.
@@ -416,7 +416,7 @@ void native_compile_binary(environment const & env, declaration const & d) {
 
     // Compute the live set of names, we attach a callback that will be
     // invoked for every declaration encountered.
-    used_defs used_names(env, [&] (used_defs & used_names, declaration const & d) {
+    used_defs used_names{env, [&] (declaration const & d) {
         buffer<procedure> procs;
         if (is_internal_decl(d)) {
             return;
@@ -432,7 +432,7 @@ void native_compile_binary(environment const & env, declaration const & d) {
                 all_procs.push_back(pair);
             }
         }
-    });
+    }};
 
     // We then loop over the set of procs produced by preprocessing the
     // main function, we transitively collect all names.
diff --git a/src/library/native_compiler/used_defs.cpp b/src/library/native_compiler/used_defs.cpp
index 451ab50e7d..b614c07c76 100644
--- a/src/library/native_compiler/used_defs.cpp
+++ b/src/library/native_compiler/used_defs.cpp
@@ -17,7 +17,7 @@ Author: Jared Roesch
 #include "library/native_compiler/used_defs.h"
 
 namespace lean {
-used_defs::used_defs(environment const & env, std::function<void(used_defs &, declaration const &)> action) : m_env(env) {
+used_defs::used_defs(environment const & env, std::function<void(declaration const &)> action) : m_env(env) {
     this->m_used_names = name_set();
     this->m_names_to_process = std::vector<name>();
     this->m_action = action;
@@ -40,7 +40,7 @@ void used_defs::empty_stack() {
         // Is a definition and not a synthetic compiler name.
         auto d = this->m_env.find(n);
         if (d && d.value().is_definition()) {
-            m_action(*this, d.value());
+            m_action(d.value());
         }
     }
 }
diff --git a/src/library/native_compiler/used_defs.h b/src/library/native_compiler/used_defs.h
index 5b9bbea386..e8960a792a 100644
--- a/src/library/native_compiler/used_defs.h
+++ b/src/library/native_compiler/used_defs.h
@@ -20,9 +20,9 @@ struct used_defs {
     name_set m_used_names;
     std::vector<name> m_names_to_process;
     environment const & m_env;
-    std::function<void(used_defs &, declaration const &)> m_action;
+    std::function<void(declaration const &)> m_action;
 
-    used_defs(environment const & env, std::function<void(used_defs &, declaration const &)>);
+    used_defs(environment const & env, std::function<void(declaration const &)>);
     void names_in_decl(declaration const & d);
     void names_in_expr(expr const & e);
     void names_in_preprocessed_body(expr const & e);