From 73eda00ba3a03acc4bc2148ab52b6e6f889bf602 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 7 Feb 2018 13:19:52 -0800
Subject: [PATCH] refactor(library/compiler): mk_unused_name ==>
 mk_compiler_unused_name

---
 src/library/compiler/elim_recursors.cpp | 2 +-
 src/library/compiler/extract_values.cpp | 2 +-
 src/library/compiler/lambda_lifting.cpp | 2 +-
 src/library/compiler/util.cpp           | 2 +-
 src/library/compiler/util.h             | 2 +-
 5 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/library/compiler/elim_recursors.cpp b/src/library/compiler/elim_recursors.cpp
index 9855249b57..284d87e5d1 100644
--- a/src/library/compiler/elim_recursors.cpp
+++ b/src/library/compiler/elim_recursors.cpp
@@ -113,7 +113,7 @@ protected:
         aux = abstract_locals(aux, abst_locals);
         /* Create expr (rec_fn) for representing recursive calls. */
         expr aux_decl_type = ctx().infer(aux);
-        name aux_decl_name = mk_unused_name(m_env, m_prefix, "_rec", m_idx);
+        name aux_decl_name = mk_compiler_unused_name(m_env, m_prefix, "_rec", m_idx);
         expr rec_fn = mk_rec_fn_macro(aux_decl_name, aux_decl_type);
         /* Create new locals for aux.
            The operating abstract_locals creates a lambda-abstraction around aux if it uses
diff --git a/src/library/compiler/extract_values.cpp b/src/library/compiler/extract_values.cpp
index 6e05bbb3f9..c358db08c5 100644
--- a/src/library/compiler/extract_values.cpp
+++ b/src/library/compiler/extract_values.cpp
@@ -24,7 +24,7 @@ class extract_values_fn : public compiler_step_visitor {
         auto it = m_cache.find(e);
         if (it != m_cache.end())
             return it->second;
-        name aux = mk_unused_name(env(), m_prefix, "_val", m_idx);
+        name aux = mk_compiler_unused_name(env(), m_prefix, "_val", m_idx);
         m_new_procs.push_back(procedure(aux, m_pos, e));
         expr r   = mk_constant(aux);
         m_cache.insert(mk_pair(e, r));
diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp
index 44e3e56e04..22fefd2f9d 100644
--- a/src/library/compiler/lambda_lifting.cpp
+++ b/src/library/compiler/lambda_lifting.cpp
@@ -129,7 +129,7 @@ class lambda_lifting_fn : public compiler_step_visitor {
 
         buffer<expr> locals;
         new_e = abstract_locals(new_e, locals);
-        name aux_name = mk_unused_name(env(), m_prefix, "_lambda", m_idx);
+        name aux_name = mk_compiler_unused_name(env(), m_prefix, "_lambda", m_idx);
         m_new_procs.emplace_back(aux_name, get_pos_info(e), new_e);
         return mk_rev_app(mk_constant(aux_name), locals);
     }
diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp
index bc01d35f4d..60ab91b140 100644
--- a/src/library/compiler/util.cpp
+++ b/src/library/compiler/util.cpp
@@ -23,7 +23,7 @@ bool is_pack_unpack(environment const & env, expr const & e) {
     return is_ginductive_pack(env, n) || is_ginductive_unpack(env, n);
 }
 
-name mk_unused_name(environment const & env, name const & prefix, char const * suffix, unsigned & idx) {
+name mk_compiler_unused_name(environment const & env, name const & prefix, char const * suffix, unsigned & idx) {
     while (true) {
         name curr(prefix, suffix);
         curr = curr.append_after(idx);
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index d90d67feff..e5e8573772 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -10,7 +10,7 @@ namespace lean {
 class type_context;
 /** \brief Create a new name of the form prefix.suffix_idx that is not the name of a declaration and/or VM function.
     It also updates the index idx. */
-name mk_unused_name(environment const & env, name const & prefix, char const * suffix, unsigned & idx);
+name mk_compiler_unused_name(environment const & env, name const & prefix, char const * suffix, unsigned & idx);
 
 /** \brief Return true iff \c e is computationally irrelevant */
 bool is_comp_irrelevant(type_context & ctx, expr const & e);