diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp index 0b57cf476..332552b3e 100644 --- a/src/frontends/lean/decl_cmds.cpp +++ b/src/frontends/lean/decl_cmds.cpp @@ -286,7 +286,7 @@ struct decl_attributes { optional m_priority; optional m_unfold_c_hint; - decl_attributes(bool def_only = true, bool is_abbrev=false):m_priority() { + decl_attributes(bool def_only = true, bool is_abbrev = false):m_priority() { m_def_only = def_only; m_is_abbrev = is_abbrev; m_is_instance = false; diff --git a/src/library/abbreviation.cpp b/src/library/abbreviation.cpp index 1c5572a3a..abbae5ca8 100644 --- a/src/library/abbreviation.cpp +++ b/src/library/abbreviation.cpp @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#include #include "util/sstream.h" #include "kernel/find_fn.h" #include "kernel/replace_fn.h"