diff --git a/src/kernel/error_msgs.cpp b/src/kernel/error_msgs.cpp index ae2d26a1c..c76145599 100644 --- a/src/kernel/error_msgs.cpp +++ b/src/kernel/error_msgs.cpp @@ -7,7 +7,7 @@ Author: Leonardo de Moura #include "kernel/error_msgs.h" namespace lean { -static format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e) { +format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e) { return nest(get_pp_indent(opts), compose(line(), fmt(env, e, opts))); } diff --git a/src/kernel/error_msgs.h b/src/kernel/error_msgs.h index 207a2aac4..a4d1ce43a 100644 --- a/src/kernel/error_msgs.h +++ b/src/kernel/error_msgs.h @@ -8,6 +8,7 @@ Author: Leonardo de Moura #include "kernel/expr.h" #include "kernel/formatter.h" namespace lean { +format pp_indent_expr(formatter const & fmt, environment const & env, options const & opts, expr const & e); format pp_type_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); format pp_function_expected(formatter const & fmt, environment const & env, options const & opts, expr const & e); format pp_app_type_mismatch(formatter const & fmt, environment const & env, options const & opts, expr const & app,