From ae52c8062ea99fb9b0dde22cb1cf6e3d02a52cd7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 12 Dec 2013 17:39:14 -0800 Subject: [PATCH] chore(kernel/metavar): remove unused function Signed-off-by: Leonardo de Moura --- src/kernel/metavar.cpp | 7 ------- src/kernel/metavar.h | 2 -- 2 files changed, 9 deletions(-) diff --git a/src/kernel/metavar.cpp b/src/kernel/metavar.cpp index dc1284aa98..66dde3469f 100644 --- a/src/kernel/metavar.cpp +++ b/src/kernel/metavar.cpp @@ -51,13 +51,6 @@ public: virtual optional get_main_expr() const { return some_expr(m_expr); } }; -void swap(metavar_env & a, metavar_env & b) { - swap(a.m_name_generator, b.m_name_generator); - swap(a.m_metavar_data, b.m_metavar_data); - std::swap(a.m_beta_reduce_mv, b.m_beta_reduce_mv); - std::swap(a.m_timestamp, b.m_timestamp); -} - void metavar_env::inc_timestamp() { if (m_timestamp == std::numeric_limits::max()) { // This should not happen in real examples. We add it just to be safe. diff --git a/src/kernel/metavar.h b/src/kernel/metavar.h index e7363a2970..12c39180e8 100644 --- a/src/kernel/metavar.h +++ b/src/kernel/metavar.h @@ -154,8 +154,6 @@ public: } }; -void swap(metavar_env & a, metavar_env & b); - /** \brief Apply the changes in \c lctx to \c a. */