diff --git a/src/kernel/builtin.cpp b/src/kernel/builtin.cpp index b05bd78ed3..a7938c5aee 100644 --- a/src/kernel/builtin.cpp +++ b/src/kernel/builtin.cpp @@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include "runtime/object.h" -using namespace lean; +using namespace lean; // NOLINT lean::object* lean_expr_local(lean::object*, lean::object*, lean::object*, lean::object*) { lean_unreachable(); diff --git a/src/library/compiler/emit_cpp.cpp b/src/library/compiler/emit_cpp.cpp index a556321de4..b47cf84492 100644 --- a/src/library/compiler/emit_cpp.cpp +++ b/src/library/compiler/emit_cpp.cpp @@ -5,6 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include +#include #include "runtime/utf8.h" #include "runtime/apply.h" #include "kernel/instantiate.h" @@ -651,7 +653,6 @@ struct emit_fn_fn { m_out << "else\n"; emit(args[2]); } else { - if (is_obj(x)) { m_out << "switch (lean::obj_tag("; emit_fvar(x); m_out << ")) {\n"; } else { diff --git a/src/library/compiler/name_mangling.cpp b/src/library/compiler/name_mangling.cpp index 5e87d0683e..a6f88ab32e 100644 --- a/src/library/compiler/name_mangling.cpp +++ b/src/library/compiler/name_mangling.cpp @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #include +#include #include "runtime/utf8.h" #include "util/name.h" diff --git a/src/library/compiler/name_mangling.h b/src/library/compiler/name_mangling.h index 811b88e1ba..efca5bb274 100644 --- a/src/library/compiler/name_mangling.h +++ b/src/library/compiler/name_mangling.h @@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ #pragma once +#include #include "util/name.h" namespace lean { diff --git a/src/library/vm/vm.cpp b/src/library/vm/vm.cpp index d80b32b03b..08638a6008 100644 --- a/src/library/vm/vm.cpp +++ b/src/library/vm/vm.cpp @@ -18,7 +18,6 @@ Author: Leonardo de Moura #include "util/name_hash_map.h" #include "util/name_hash_set.h" #include "util/timeit.h" -#include "util/name_hash_map.h" #include "util/sexpr/option_declarations.h" #include "util/shared_mutex.h" #include "library/constants.h"