From 42e253c96205789d52bef398346e9b49f61a8bca Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 22 Feb 2014 08:42:08 -0800
Subject: [PATCH] fix(*): style and clang warnings

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/kernel/level.cpp         | 2 +-
 src/tests/util/exception.cpp | 3 +--
 src/util/name_generator.cpp  | 1 +
 src/util/rb_tree.h           | 6 ++++--
 4 files changed, 7 insertions(+), 5 deletions(-)

diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 0bc143d88..d7e6a1d14 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -339,7 +339,7 @@ class level_deserializer : public object_deserializer<level> {
     typedef object_deserializer<level> super;
 public:
     level read() {
-        return super::read([&]() {
+        return super::read([&]() -> level {
                 deserializer & d = get_owner();
                 auto k = static_cast<level_kind>(d.read_char());
                 switch (k) {
diff --git a/src/tests/util/exception.cpp b/src/tests/util/exception.cpp
index cfb48024e..df2d26649 100644
--- a/src/tests/util/exception.cpp
+++ b/src/tests/util/exception.cpp
@@ -45,9 +45,8 @@ static void tst4() {
 
 class ex : public exception {
     std::function<char const *()> m_f;
-    ex(std::function<char const *()> const & f):m_f(f) {}
 public:
-    template<typename F> ex(F && f):m_f(f) {}
+    ex(std::function<char const *()> const & f):m_f(f) {}
     virtual exception * clone() const { return new ex(m_f); }
     virtual void rethrow() const { throw *this; }
     virtual char const * what() const noexcept { return m_f(); }
diff --git a/src/util/name_generator.cpp b/src/util/name_generator.cpp
index e8e9b58ba..55ef733ee 100644
--- a/src/util/name_generator.cpp
+++ b/src/util/name_generator.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
+#include <algorithm>
 #include "util/name_generator.h"
 
 namespace lean {
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index 2d8670b69..514356966 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <utility>
+#include <algorithm>
 #include "util/rc.h"
 #include "util/debug.h"
 #include "util/buffer.h"
@@ -69,8 +70,9 @@ class rb_tree : public CMP {
         if (n.is_shared()) {
             // std::cout << "SHARED\n";
             return node(new node_cell(*n.m_ptr));
-        } else
+        } else {
             return n;
+        }
     }
 
     static node set_black(node && n) {
@@ -290,7 +292,7 @@ public:
         lean_assert(check_invariant());
     }
 
-    void erase_min(T const & v) {
+    void erase_min() {
         m_root = set_black(erase_min(m_root.steal()));
         lean_assert(check_invariant());
     }