diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 8ccba6729..d23991e4b 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -5,6 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <deque>
+#include <limits>
+#include <utility>
+#include <vector>
 #include "util/flet.h"
 #include "kernel/normalizer.h"
 #include "kernel/context.h"
diff --git a/src/frontends/lean/elaborator_exception.cpp b/src/frontends/lean/elaborator_exception.cpp
index 87ebb81e6..ac21c5158 100644
--- a/src/frontends/lean/elaborator_exception.cpp
+++ b/src/frontends/lean/elaborator_exception.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
 #include "frontends/lean/elaborator_exception.h"
 #include "frontends/lean/elaborator.h"
 
diff --git a/src/frontends/lean/elaborator_exception.h b/src/frontends/lean/elaborator_exception.h
index a2b03a2f1..547a4e162 100644
--- a/src/frontends/lean/elaborator_exception.h
+++ b/src/frontends/lean/elaborator_exception.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <vector>
 #include "kernel/kernel_exception.h"
 #include "library/state.h"
 #include "frontends/lean/elaborator.h"
diff --git a/src/frontends/lean/frontend.cpp b/src/frontends/lean/frontend.cpp
index 2e3ef8acb..67d4d0122 100644
--- a/src/frontends/lean/frontend.cpp
+++ b/src/frontends/lean/frontend.cpp
@@ -6,6 +6,10 @@ Author: Leonardo de Moura
 */
 #include <atomic>
 #include <unordered_set>
+#include <vector>
+#include <utility>
+#include <functional>
+
 #include "util/map.h"
 #include "util/sstream.h"
 #include "util/exception.h"
diff --git a/src/frontends/lean/operator_info.h b/src/frontends/lean/operator_info.h
index 8da83514c..686b1dc92 100644
--- a/src/frontends/lean/operator_info.h
+++ b/src/frontends/lean/operator_info.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <algorithm>
 #include "util/name.h"
 #include "util/list.h"
 #include "util/sexpr/format.h"
diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index e0e9c5949..56b368e18 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -4,7 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#ifdef LEAN_USE_READLINE
+#include <stdlib.h>
+#include <stdio.h>
+#include <unistd.h>
+#include <readline/readline.h>
+#include <readline/history.h>
+#endif
 #include <unordered_map>
+#include <utility>
+#include <string>
+#include <vector>
 #include "util/scoped_map.h"
 #include "util/exception.h"
 #include "util/sstream.h"
@@ -27,13 +37,6 @@ Author: Leonardo de Moura
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/notation.h"
 #include "frontends/lean/pp.h"
-#ifdef LEAN_USE_READLINE
-#include <stdlib.h>
-#include <stdio.h>
-#include <unistd.h>
-#include <readline/readline.h>
-#include <readline/history.h>
-#endif
 
 #ifndef LEAN_DEFAULT_PARSER_SHOW_ERRORS
 #define LEAN_DEFAULT_PARSER_SHOW_ERRORS true
diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index 8266ee7d7..3d4c292f0 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include <memory>
+#include <utility>
+#include <vector>
 #include "util/scoped_map.h"
 #include "util/exception.h"
 #include "util/scoped_set.h"
diff --git a/src/frontends/lean/scanner.h b/src/frontends/lean/scanner.h
index 1ef34ec4d..39fbe4ded 100644
--- a/src/frontends/lean/scanner.h
+++ b/src/frontends/lean/scanner.h
@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <vector>
+#include <string>
 #include "util/name.h"
 #include "util/list.h"
 #include "util/numerics/mpq.h"
diff --git a/src/interval/interval_def.h b/src/interval/interval_def.h
index 1847ef8f1..04064de5f 100644
--- a/src/interval/interval_def.h
+++ b/src/interval/interval_def.h
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <gmp.h>
 #include <mpfr.h>
 #include <utility>
+#include <algorithm>
 #include "util/trace.h"
 #include "util/numerics/mpz.h"
 #include "interval/interval.h"
diff --git a/src/kernel/abstract.cpp b/src/kernel/abstract.cpp
index ad14c325c..c3366087e 100644
--- a/src/kernel/abstract.cpp
+++ b/src/kernel/abstract.cpp
@@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
-#include "abstract.h"
-#include "free_vars.h"
-#include "replace.h"
+#include <utility>
+#include "kernel/abstract.h"
+#include "kernel/free_vars.h"
+#include "kernel/replace.h"
 
 namespace lean {
 expr abstract(expr const & e, unsigned n, expr const * s) {
diff --git a/src/kernel/abstract.h b/src/kernel/abstract.h
index 8437ae0b1..77cab363d 100644
--- a/src/kernel/abstract.h
+++ b/src/kernel/abstract.h
@@ -5,7 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
+#include <utility>
+#include "kernel/expr.h"
 
 namespace lean {
 /**
diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp
index 1aff0064e..6af91a98d 100644
--- a/src/kernel/builtin.cpp
+++ b/src/kernel/builtin.cpp
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "builtin.h"
-#include "environment.h"
-#include "abstract.h"
+#include "kernel/builtin.h"
+#include "kernel/environment.h"
+#include "kernel/abstract.h"
 
 #ifndef LEAN_DEFAULT_LEVEL_SEPARATION
 #define LEAN_DEFAULT_LEVEL_SEPARATION 512
diff --git a/src/kernel/builtin.h b/src/kernel/builtin.h
index ce248b011..0be24aae6 100644
--- a/src/kernel/builtin.h
+++ b/src/kernel/builtin.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
+#include "kernel/expr.h"
 
 namespace lean {
 /**
diff --git a/src/kernel/context.cpp b/src/kernel/context.cpp
index 2ebdb462d..33a5904fe 100644
--- a/src/kernel/context.cpp
+++ b/src/kernel/context.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <utility>
 #include "util/exception.h"
 #include "kernel/context.h"
 
diff --git a/src/kernel/context.h b/src/kernel/context.h
index b0bb98c59..937b752be 100644
--- a/src/kernel/context.h
+++ b/src/kernel/context.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <utility>
 #include "util/list.h"
 #include "kernel/expr.h"
 
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 4bc0ec6ea..f216f3840 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -7,9 +7,9 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <memory>
-#include "context.h"
-#include "object.h"
-#include "level.h"
+#include "kernel/context.h"
+#include "kernel/object.h"
+#include "kernel/level.h"
 
 namespace lean {
 /**
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 90bf973ca..3d8ead848 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <limits>
 #include <atomic>
+#include <utility>
 #include "util/rc.h"
 #include "util/name.h"
 #include "util/hash.h"
diff --git a/src/kernel/expr_maps.h b/src/kernel/expr_maps.h
index 0ad2c5311..9fd757ea8 100644
--- a/src/kernel/expr_maps.h
+++ b/src/kernel/expr_maps.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <unordered_map>
-#include "expr.h"
+#include "kernel/expr.h"
 
 namespace lean {
 
diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h
index 93a923305..676bb5c56 100644
--- a/src/kernel/expr_sets.h
+++ b/src/kernel/expr_sets.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <unordered_set>
+#include <utility>
 #include "util/hash.h"
 #include "kernel/expr.h"
 
diff --git a/src/kernel/for_each.h b/src/kernel/for_each.h
index 609eadd6d..4fe847daf 100644
--- a/src/kernel/for_each.h
+++ b/src/kernel/for_each.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
-#include "expr_sets.h"
+#include "kernel/expr.h"
+#include "kernel/expr_sets.h"
 
 namespace lean {
 template<typename F>
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index e4f6a145a..3ab732ec3 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
-#include "free_vars.h"
-#include "expr_sets.h"
-#include "replace.h"
+#include "kernel/free_vars.h"
+#include "kernel/expr_sets.h"
+#include "kernel/replace.h"
 
 namespace lean {
 
diff --git a/src/kernel/free_vars.h b/src/kernel/free_vars.h
index 63c1be127..95471fdbf 100644
--- a/src/kernel/free_vars.h
+++ b/src/kernel/free_vars.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
+#include "kernel/expr.h"
 namespace lean {
 /**
    \brief Return true iff the given expression has free variables.
diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
index 1f1694810..94ad56653 100644
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
+#include "kernel/expr.h"
 
 namespace lean {
 /**
diff --git a/src/kernel/kernel_exception.h b/src/kernel/kernel_exception.h
index 932dcb5e0..7bec23642 100644
--- a/src/kernel/kernel_exception.h
+++ b/src/kernel/kernel_exception.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <vector>
 #include "util/exception.h"
 #include "kernel/context.h"
 #include "kernel/environment.h"
diff --git a/src/kernel/normalizer.cpp b/src/kernel/normalizer.cpp
index bdc0b16c6..418f66b58 100644
--- a/src/kernel/normalizer.cpp
+++ b/src/kernel/normalizer.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
+#include <limits>
 #include "util/scoped_map.h"
 #include "util/list.h"
 #include "util/flet.h"
diff --git a/src/kernel/normalizer.h b/src/kernel/normalizer.h
index 0f1d0badb..c7908069f 100644
--- a/src/kernel/normalizer.h
+++ b/src/kernel/normalizer.h
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
-#include "expr.h"
-#include "environment.h"
-#include "context.h"
+#include "kernel/expr.h"
+#include "kernel/environment.h"
+#include "kernel/context.h"
 
 namespace lean {
 class environment;
diff --git a/src/kernel/object.h b/src/kernel/object.h
index 14b8c343d..f54e5fcd3 100644
--- a/src/kernel/object.h
+++ b/src/kernel/object.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <algorithm>
 #include "util/rc.h"
 #include "kernel/expr.h"
 /*
diff --git a/src/kernel/occurs.cpp b/src/kernel/occurs.cpp
index 0f00f5cd4..96b3ddb7c 100644
--- a/src/kernel/occurs.cpp
+++ b/src/kernel/occurs.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "occurs.h"
-#include "for_each.h"
+#include "kernel/occurs.h"
+#include "kernel/for_each.h"
 
 namespace lean {
 template<typename F>
diff --git a/src/kernel/occurs.h b/src/kernel/occurs.h
index a169c498a..448e064da 100644
--- a/src/kernel/occurs.h
+++ b/src/kernel/occurs.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "context.h"
+#include "kernel/context.h"
 
 namespace lean {
 /** \brief Return true iff \c n occurs in \c m */
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 543768879..b678d60b5 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <memory>
-#include "expr.h"
-#include "context.h"
+#include "kernel/expr.h"
+#include "kernel/context.h"
 
 namespace lean {
 class environment;
diff --git a/src/kernel/value.h b/src/kernel/value.h
index 628b50790..095432b97 100644
--- a/src/kernel/value.h
+++ b/src/kernel/value.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "expr.h"
+#include "kernel/expr.h"
 
 namespace lean {
 // Some value subclasses that capture common implementation patterns.
diff --git a/src/library/expr_pair.h b/src/library/expr_pair.h
index 2694406aa..f37fb7dbc 100644
--- a/src/library/expr_pair.h
+++ b/src/library/expr_pair.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <utility>
 #include "util/hash.h"
 #include "kernel/expr.h"
 
diff --git a/src/library/kernel_exception_formatter.cpp b/src/library/kernel_exception_formatter.cpp
index 4fdd96af2..5c198608e 100644
--- a/src/library/kernel_exception_formatter.cpp
+++ b/src/library/kernel_exception_formatter.cpp
@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include <vector>
 #include "library/kernel_exception_formatter.h"
 
 namespace lean {
diff --git a/src/library/printer.cpp b/src/library/printer.cpp
index e403c8738..99a606699 100644
--- a/src/library/printer.cpp
+++ b/src/library/printer.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
+#include <utility>
 #include "util/exception.h"
 #include "library/printer.h"
 #include "library/metavar.h"
diff --git a/src/library/printer.h b/src/library/printer.h
index 057a5a1dc..f13d736b6 100644
--- a/src/library/printer.h
+++ b/src/library/printer.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
+#include <utility>
 #include "kernel/expr.h"
 #include "kernel/context.h"
 
diff --git a/src/tests/interval/check.h b/src/tests/interval/check.h
index 3d6af192e..f58b809ee 100644
--- a/src/tests/interval/check.h
+++ b/src/tests/interval/check.h
@@ -1,3 +1,5 @@
+#include <string>
+
 using std::cout;
 using std::endl;
 
diff --git a/src/util/buffer.h b/src/util/buffer.h
index 96b9cc628..1e349d6a8 100644
--- a/src/util/buffer.h
+++ b/src/util/buffer.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <algorithm>
 #include <cstring>
-#include "debug.h"
+#include "util/debug.h"
 
 namespace lean {
 /**
diff --git a/src/util/debug.cpp b/src/util/debug.cpp
index 6653b130b..904160242 100644
--- a/src/util/debug.cpp
+++ b/src/util/debug.cpp
@@ -4,18 +4,17 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "debug.h"
 #include <iostream>
 #include <sstream>
 #include <set>
 #include <string>
 #include <memory>
 #include <cstdlib>
-
 #ifndef _WINDOWS
 // Support for pid
 #include<unistd.h>
 #endif
+#include "util/debug.h"
 
 namespace lean {
 static volatile bool                          g_has_violations    = false;
diff --git a/src/util/escaped.cpp b/src/util/escaped.cpp
index 3c9a1abaf..53a02688e 100644
--- a/src/util/escaped.cpp
+++ b/src/util/escaped.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "escaped.h"
+#include "util/escaped.h"
 
 namespace lean {
 
diff --git a/src/util/exception.cpp b/src/util/exception.cpp
index d7c180501..674c87cfe 100644
--- a/src/util/exception.cpp
+++ b/src/util/exception.cpp
@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <sstream>
-#include "exception.h"
-#include "sstream.h"
+#include <string>
+#include "util/exception.h"
+#include "util/sstream.h"
 
 namespace lean {
 
diff --git a/src/util/hash.h b/src/util/hash.h
index e015aaffb..e3eab34d3 100644
--- a/src/util/hash.h
+++ b/src/util/hash.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "debug.h"
+#include "util/debug.h"
 
 namespace lean {
 
diff --git a/src/util/list.h b/src/util/list.h
index ae23a8f4f..bfafcd63b 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <iterator>
-#include "rc.h"
-#include "debug.h"
+#include "util/rc.h"
+#include "util/debug.h"
 
 namespace lean {
 /**
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index bf42f2804..2909dbfca 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include "list.h"
-#include "buffer.h"
-#include "pair.h"
+#include <utility>
+#include "util/list.h"
+#include "util/buffer.h"
+#include "util/pair.h"
 
 namespace lean {
 /**
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 0cfa6be66..923e7f315 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -8,13 +8,14 @@ Author: Leonardo de Moura
 #include <vector>
 #include <algorithm>
 #include <sstream>
-#include "name.h"
-#include "debug.h"
-#include "rc.h"
-#include "buffer.h"
-#include "hash.h"
-#include "trace.h"
-#include "ascii.h"
+#include <string>
+#include "util/name.h"
+#include "util/debug.h"
+#include "util/rc.h"
+#include "util/buffer.h"
+#include "util/hash.h"
+#include "util/trace.h"
+#include "util/ascii.h"
 
 namespace lean {
 constexpr char const * anonymous_str = "[anonymous]";
diff --git a/src/util/name.h b/src/util/name.h
index ad869c280..75c0a359f 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
+#include <string>
 #include <iostream>
 
 namespace lean {
diff --git a/src/util/name_set.h b/src/util/name_set.h
index b2c382270..c4ef2bcc8 100644
--- a/src/util/name_set.h
+++ b/src/util/name_set.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <unordered_set>
-#include "name.h"
+#include "util/name.h"
 namespace lean {
 typedef std::unordered_set<name, name_hash, name_eq> name_set;
 }
diff --git a/src/util/numerics/double.cpp b/src/util/numerics/double.cpp
index aaabd97bb..87930b928 100644
--- a/src/util/numerics/double.cpp
+++ b/src/util/numerics/double.cpp
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Soonho Kong
 */
+#include <cmath>
 #include "util/numerics/numeric_traits.h"
 #include "util/numerics/double.h"
-#include <cmath>
 
 namespace lean {
 
diff --git a/src/util/numerics/float.cpp b/src/util/numerics/float.cpp
index 2a273722c..42bdd318d 100644
--- a/src/util/numerics/float.cpp
+++ b/src/util/numerics/float.cpp
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Soonho Kong
 */
+#include <cmath>
 #include "util/numerics/numeric_traits.h"
 #include "util/numerics/float.h"
-#include <cmath>
 
 namespace lean {
 
diff --git a/src/util/numerics/gmp_init.cpp b/src/util/numerics/gmp_init.cpp
index e2b9b874c..5aec8e7a0 100644
--- a/src/util/numerics/gmp_init.cpp
+++ b/src/util/numerics/gmp_init.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <new>
 #include <gmp.h>
+#include <new>
 #include <cstdlib>
 
 extern "C" void * cxx_malloc(size_t size) {
diff --git a/src/util/numerics/mpfp.cpp b/src/util/numerics/mpfp.cpp
index 076d880d3..0101ed2cc 100644
--- a/src/util/numerics/mpfp.cpp
+++ b/src/util/numerics/mpfp.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Soonho Kong
 */
 #include <cmath>
+#include <string>
 #include "util/numerics/mpfp.h"
 
 namespace lean {
diff --git a/src/util/numerics/mpz.cpp b/src/util/numerics/mpz.cpp
index 4b8ce400c..006514b88 100644
--- a/src/util/numerics/mpz.cpp
+++ b/src/util/numerics/mpz.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <memory>
-#include "mpz.h"
+#include "util/numerics/mpz.h"
 
 namespace lean {
 
diff --git a/src/util/numerics/mpz.h b/src/util/numerics/mpz.h
index eecb7bb06..8cfd2bc46 100644
--- a/src/util/numerics/mpz.h
+++ b/src/util/numerics/mpz.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <iostream>
 #include <gmp.h>
+#include <iostream>
 #include "util/debug.h"
 #include "util/numerics/numeric_traits.h"
 
diff --git a/src/util/numerics/numeric_traits.cpp b/src/util/numerics/numeric_traits.cpp
index 8a230f2e6..8e3590d2e 100644
--- a/src/util/numerics/numeric_traits.cpp
+++ b/src/util/numerics/numeric_traits.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 */
 #include <cfenv>
 #include <cmath>
-#include "numeric_traits.h"
+#include "util/numerics/numeric_traits.h"
 
 namespace lean {
 
diff --git a/src/util/output_channel.h b/src/util/output_channel.h
index 06f710e62..54022af80 100644
--- a/src/util/output_channel.h
+++ b/src/util/output_channel.h
@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <fstream>
 #include <sstream>
+#include <string>
 
 namespace lean {
 /**
diff --git a/src/util/pdeque.h b/src/util/pdeque.h
index 2ce8ee5cb..3d681f7fe 100644
--- a/src/util/pdeque.h
+++ b/src/util/pdeque.h
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <iostream>
 #include <deque>
-#include "rc.h"
+#include <iostream>
+#include "util/rc.h"
 
 #ifndef LEAN_PDEQUE_MIN_QUOTA
 #define LEAN_PDEQUE_MIN_QUOTA 16
diff --git a/src/util/pvector.h b/src/util/pvector.h
index cb55324d5..34cb0db5b 100644
--- a/src/util/pvector.h
+++ b/src/util/pvector.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <vector>
-#include "rc.h"
+#include "util/rc.h"
 
 #ifndef LEAN_PVECTOR_MIN_QUOTA
 #define LEAN_PVECTOR_MIN_QUOTA 16
diff --git a/src/util/rc.h b/src/util/rc.h
index 66af36c0b..0ca974a0f 100644
--- a/src/util/rc.h
+++ b/src/util/rc.h
@@ -7,9 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 
 // Goodies for reference counting
-
-#include "debug.h"
-
 #ifdef LEAN_THREAD_UNSAFE_REF_COUNT
 #define MK_LEAN_RC()                                                    \
 private:                                                                \
@@ -30,6 +27,7 @@ void inc_ref() { std::atomic_fetch_add_explicit(&m_rc, 1u, std::memory_order_rel
 bool dec_ref_core() { lean_assert(get_rc() > 0); return std::atomic_fetch_sub_explicit(&m_rc, 1u, std::memory_order_relaxed) == 1u; } \
 void dec_ref() { if (dec_ref_core()) dealloc(); }
 #endif
+#include "util/debug.h"
 
 #define LEAN_COPY_REF(T, Arg)                   \
     if (Arg.m_ptr)                              \
diff --git a/src/util/safe_arith.cpp b/src/util/safe_arith.cpp
index cc9b62b22..d2eef2c10 100644
--- a/src/util/safe_arith.cpp
+++ b/src/util/safe_arith.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
-#include "exception.h"
+#include "util/exception.h"
 
 namespace lean {
 void check_int_overflow(long long n) {
diff --git a/src/util/scoped_map.h b/src/util/scoped_map.h
index 122c91431..683d6eab7 100644
--- a/src/util/scoped_map.h
+++ b/src/util/scoped_map.h
@@ -8,7 +8,9 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <unordered_map>
 #include <vector>
-#include "debug.h"
+#include <utility>
+#include <functional>
+#include "util/debug.h"
 
 #ifndef LEAN_SCOPED_MAP_INITIAL_BUCKET_SIZE
 #define LEAN_SCOPED_MAP_INITIAL_BUCKET_SIZE 8
diff --git a/src/util/scoped_set.h b/src/util/scoped_set.h
index f390b5ec4..22518bba6 100644
--- a/src/util/scoped_set.h
+++ b/src/util/scoped_set.h
@@ -7,7 +7,9 @@ Author: Leonardo de Moura
 #pragma once
 #include <unordered_set>
 #include <vector>
-#include "debug.h"
+#include <utility>
+#include <functional>
+#include "util/debug.h"
 
 #ifndef LEAN_SCOPED_SET_INITIAL_BUCKET_SIZE
 #define LEAN_SCOPED_SET_INITIAL_BUCKET_SIZE 8
diff --git a/src/util/sexpr/format.cpp b/src/util/sexpr/format.cpp
index b5f322781..cec9f6c91 100644
--- a/src/util/sexpr/format.cpp
+++ b/src/util/sexpr/format.cpp
@@ -5,6 +5,8 @@
   Author: Soonho Kong
 */
 #include <sstream>
+#include <string>
+#include <utility>
 #include "util/escaped.h"
 #include "util/sexpr/sexpr.h"
 #include "util/sexpr/format.h"
@@ -365,7 +367,7 @@ format operator+(format const & f1, format const & f2) {
 }
 
 format operator^(format const & f1, format const & f2) {
-    return format{f1, format(" "), f2};
+    return format {f1, format(" "), f2};
 }
 
 std::ostream & pretty(std::ostream & out, unsigned w, bool colors, format const & f) {
diff --git a/src/util/sexpr/format.h b/src/util/sexpr/format.h
index 84c992d23..f5e966dfe 100644
--- a/src/util/sexpr/format.h
+++ b/src/util/sexpr/format.h
@@ -9,6 +9,8 @@ Author: Soonho Kong
 #include <iostream>
 #include <numeric>
 #include <sstream>
+#include <utility>
+#include <string>
 #include "util/pair.h"
 #include "util/debug.h"
 #include "util/numerics/mpz.h"
diff --git a/src/util/sexpr/options.cpp b/src/util/sexpr/options.cpp
index 30c5c2a8c..a1d8a82df 100644
--- a/src/util/sexpr/options.cpp
+++ b/src/util/sexpr/options.cpp
@@ -5,9 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <memory>
-#include "options.h"
-#include "option_declarations.h"
-#include "sexpr_fn.h"
+#include <string>
+#include "util/sexpr/options.h"
+#include "util/sexpr/option_declarations.h"
+#include "util/sexpr/sexpr_fn.h"
 
 namespace lean {
 std::ostream & operator<<(std::ostream & out, option_kind k) {
diff --git a/src/util/sexpr/sexpr.cpp b/src/util/sexpr/sexpr.cpp
index 5ea192312..d2a322046 100644
--- a/src/util/sexpr/sexpr.cpp
+++ b/src/util/sexpr/sexpr.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <cstring>
+#include <string>
 #include "util/rc.h"
 #include "util/hash.h"
 #include "util/name.h"
diff --git a/src/util/sexpr/sexpr.h b/src/util/sexpr/sexpr.h
index eb2a6f09f..002ef8dc1 100644
--- a/src/util/sexpr/sexpr.h
+++ b/src/util/sexpr/sexpr.h
@@ -6,6 +6,8 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
+#include <string>
+#include <algorithm>
 
 namespace lean {
 class name;
diff --git a/src/util/sexpr/sexpr_fn.cpp b/src/util/sexpr/sexpr_fn.cpp
index ad2b8578a..a6a7b7882 100644
--- a/src/util/sexpr/sexpr_fn.cpp
+++ b/src/util/sexpr/sexpr_fn.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "sexpr_fn.h"
+#include "util/sexpr/sexpr_fn.h"
 
 namespace lean {
 
diff --git a/src/util/sstream.h b/src/util/sstream.h
index fee14148a..6d5c6a6cc 100644
--- a/src/util/sstream.h
+++ b/src/util/sstream.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <sstream>
+#include <string>
 
 namespace lean {
 /** \brief Wrapper for std::ostringstream */
diff --git a/src/util/test.h b/src/util/test.h
index c9151a68c..5d0a59c3d 100644
--- a/src/util/test.h
+++ b/src/util/test.h
@@ -9,4 +9,4 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEBUG
 #define LEAN_DEBUG
 #endif
-#include "debug.h"
+#include "util/debug.h"
diff --git a/src/util/timeit.h b/src/util/timeit.h
index d668e6206..fe547e24c 100644
--- a/src/util/timeit.h
+++ b/src/util/timeit.h
@@ -5,8 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <iostream>
 #include <time.h>
+#include <string>
+#include <iostream>
 
 namespace lean {
 /**
diff --git a/src/util/trace.cpp b/src/util/trace.cpp
index c3eac10ff..76e44167c 100644
--- a/src/util/trace.cpp
+++ b/src/util/trace.cpp
@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 
-#include "trace.h"
 #include <set>
 #include <string>
 #include <memory>
+#include "util/trace.h"
 
 #ifndef LEAN_TRACE_OUT
 #define LEAN_TRACE_OUT ".lean_trace"
diff --git a/src/util/trace.h b/src/util/trace.h
index e8de5e140..e9d276794 100644
--- a/src/util/trace.h
+++ b/src/util/trace.h
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 
 #ifdef LEAN_TRACE
-#include <fstream>
 #include <mutex>
+#include <fstream>
 namespace lean {
 extern std::ofstream tout;
 extern std::mutex    trace_mutex;