From 74192b0cb83ea29e77cc4db38a76426c6a112725 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 11 Feb 2016 18:08:44 -0800
Subject: [PATCH] chore(library): remove dead code

---
 src/library/match.cpp      | 32 --------------------------------
 src/library/scoped_ext.cpp |  7 -------
 2 files changed, 39 deletions(-)

diff --git a/src/library/match.cpp b/src/library/match.cpp
index 2312f92b96..81ab796179 100644
--- a/src/library/match.cpp
+++ b/src/library/match.cpp
@@ -398,36 +398,4 @@ bool whnf_match_plugin::on_failure(expr const & p, expr const & t, match_context
         return false;
     }
 }
-
-static unsigned updt_idx_meta_univ_range(level const & l, unsigned r) {
-    for_each(l, [&](level const & l) {
-            if (!has_meta(l)) return false;
-            if (is_idx_metauniv(l)) {
-                unsigned new_r = to_meta_idx(l) + 1;
-                if (new_r > r)
-                    r = new_r;
-            }
-            return true;
-        });
-    return r;
-}
-
-static pair<unsigned, unsigned> get_idx_meta_univ_ranges(expr const & e) {
-    if (!has_metavar(e))
-        return mk_pair(0, 0);
-    unsigned rlvl = 0;
-    unsigned rexp = 0;
-    for_each(e, [&](expr const & e, unsigned) {
-            if (!has_metavar(e)) return false;
-            if (is_constant(e))
-                for (level const & l : const_levels(e))
-                    rlvl = updt_idx_meta_univ_range(l, rlvl);
-            if (is_sort(e))
-                rlvl = updt_idx_meta_univ_range(sort_level(e), rlvl);
-            if (is_idx_metavar(e))
-                rexp = std::max(to_meta_idx(e) + 1, rexp);
-            return true;
-        });
-    return mk_pair(rlvl, rexp);
-}
 }
diff --git a/src/library/scoped_ext.cpp b/src/library/scoped_ext.cpp
index 2bbb6cafba..25c1bad4e4 100644
--- a/src/library/scoped_ext.cpp
+++ b/src/library/scoped_ext.cpp
@@ -91,13 +91,6 @@ environment using_namespace(environment const & env, io_state const & ios, name
     return r;
 }
 
-static environment using_namespace(environment const & env, io_state const & ios, name const & n, name const & metaclass) {
-    buffer<name> tmp;
-    if (!metaclass.is_anonymous())
-        tmp.push_back(metaclass);
-    return using_namespace(env, ios, n, tmp);
-}
-
 environment using_namespace(environment const & env, io_state const & ios, name const & n) {
     buffer<name> metaclasses;
     return using_namespace(env, ios, n, metaclasses);