diff --git a/src/library/blast/context.cpp b/src/library/blast/context.cpp index 5c1b766f2..e3cfa2580 100644 --- a/src/library/blast/context.cpp +++ b/src/library/blast/context.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "library/kernel_serializer.h" #include "library/blast/context.h" diff --git a/src/library/blast/state.h b/src/library/blast/state.h index 69fa2f032..751620c72 100644 --- a/src/library/blast/state.h +++ b/src/library/blast/state.h @@ -10,6 +10,5 @@ Author: Leonardo de Moura namespace lean { namespace blast { class state { - }; }} diff --git a/src/runtime/cpp/lean_runtime.cpp b/src/runtime/cpp/lean_runtime.cpp index 026ae715b..ed4d06663 100644 --- a/src/runtime/cpp/lean_runtime.cpp +++ b/src/runtime/cpp/lean_runtime.cpp @@ -68,7 +68,7 @@ void * alloc_obj(unsigned n) { obj_cell::obj_cell(unsigned cidx, unsigned sz, obj const * fs): m_rc(0), m_kind(static_cast(obj_kind::Constructor)), m_size(sz), m_cidx(cidx) { - static_assert(sizeof(obj_cell) % sizeof(void*) == 0); // make sure the hack used to store obj_cell fields satisfies alignment constraints. + static_assert(sizeof(obj_cell) % sizeof(void*) == 0); // make sure the hack used to store obj_cell fields satisfies alignment constraints. // NOLINT void ** mem = field_addr(); for (unsigned i = 0; i < sz; i++, mem++) new (mem) obj(fs[i]);