diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index 695d9b1164..2aae4ac143 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -3298,7 +3298,7 @@ public: return static_cast(m_idx2name.size()); } - name const & get_name(unsigned idx) { + name get_name(unsigned idx) { shared_lock lock(m_mutex); lean_assert(idx < m_idx2name.size()); return m_idx2name.at(idx); @@ -3321,7 +3321,7 @@ unsigned get_vm_index(name const & n) { unsigned get_vm_index_bound() { return g_vm_index_manager->get_index_bound(); } -name const & get_vm_name(unsigned idx) { +name get_vm_name(unsigned idx) { return g_vm_index_manager->get_name(idx); } optional find_vm_name(unsigned idx) { diff --git a/src/library/vm/vm.h b/src/library/vm/vm.h index a435a3ba80..5982accc74 100644 --- a/src/library/vm/vm.h +++ b/src/library/vm/vm.h @@ -828,7 +828,7 @@ environment add_native(environment const & env, name const & n, unsigned arity, unsigned get_vm_index(name const & n); unsigned get_vm_index_bound(); -name const & get_vm_name(unsigned idx); +name get_vm_name(unsigned idx); optional find_vm_name(unsigned idx); /** \brief Reserve an index for the given function in the VM, the expression