From 165e2d5b97086211fc913598fefaa7cc56a0a0f9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 19 Sep 2016 17:36:28 -0700
Subject: [PATCH] chore(*): fix compilation warnings

---
 src/frontends/lean/inductive_cmds.cpp   | 1 -
 src/library/inductive_compiler/util.cpp | 4 ++--
 src/library/reducible.cpp               | 2 +-
 src/util/subscripted_name_set.cpp       | 2 +-
 4 files changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/frontends/lean/inductive_cmds.cpp b/src/frontends/lean/inductive_cmds.cpp
index 92f9582cde..a69758e981 100644
--- a/src/frontends/lean/inductive_cmds.cpp
+++ b/src/frontends/lean/inductive_cmds.cpp
@@ -71,7 +71,6 @@ class inductive_cmd_fn {
     level                           m_u; // temporary auxiliary global universe used for inferring the result
                                          // universe of an inductive datatype declaration.
     bool                            m_infer_result_universe{false};
-    bool                            m_found_nested_universe{false};
 
     [[ noreturn ]] void throw_error(char const * error_msg) const { throw parser_error(error_msg, m_pos); }
     [[ noreturn ]] void throw_error(sstream const & strm) const { throw parser_error(strm, m_pos); }
diff --git a/src/library/inductive_compiler/util.cpp b/src/library/inductive_compiler/util.cpp
index 9660bf3327..875be6f2f8 100644
--- a/src/library/inductive_compiler/util.cpp
+++ b/src/library/inductive_compiler/util.cpp
@@ -49,8 +49,8 @@ void assert_no_locals(name const & n, expr const & e) {
     lean_assert(false);
 }
 
-void assert_def_eq(environment const & env, expr const & e1, expr const & e2) {
-    type_checker checker(env);
+void assert_def_eq(environment const & DEBUG_CODE(env), expr const & DEBUG_CODE(e1), expr const & DEBUG_CODE(e2)) {
+    DEBUG_CODE(type_checker checker(env););
     try {
         lean_assert(checker.is_def_eq(e1, e2));
     } catch (exception ex) {
diff --git a/src/library/reducible.cpp b/src/library/reducible.cpp
index 1c83aea5d9..e3f28a9b59 100644
--- a/src/library/reducible.cpp
+++ b/src/library/reducible.cpp
@@ -49,7 +49,7 @@ public:
     reducibility_proxy_attribute(char const * id, char const * descr, reducible_status m_status):
         parent(id, descr, m_status) {}
 
-    virtual typed_attribute<reducibility_attribute_data> const & get_attribute() const {
+    virtual typed_attribute<reducibility_attribute_data> const & get_attribute() const override {
         return get_reducibility_attribute();
     }
 
diff --git a/src/util/subscripted_name_set.cpp b/src/util/subscripted_name_set.cpp
index fad19ac18f..a1ddeaf02a 100644
--- a/src/util/subscripted_name_set.cpp
+++ b/src/util/subscripted_name_set.cpp
@@ -13,7 +13,7 @@ void subscripted_name_set::check_invariants() const {
        if (auto is_subscripted = n.is_subscripted()) {
            auto subscripts = m_prefixes.find(is_subscripted->first);
            lean_assert(subscripts);
-           auto free_region = subscripts->find_next_greater_or_equal(closed_ival(is_subscripted->second));
+           DEBUG_CODE(auto free_region =) subscripts->find_next_greater_or_equal(closed_ival(is_subscripted->second));
            lean_assert(free_region);
            lean_assert(!free_region->contains(is_subscripted->second));
        }