diff --git a/src/library/local_context.cpp b/src/library/local_context.cpp index 5da87e9212..b3e620bac4 100644 --- a/src/library/local_context.cpp +++ b/src/library/local_context.cpp @@ -337,7 +337,7 @@ bool local_context::well_formed(expr const & e) const { return ok; } -format local_context::pp(formatter const & fmt, std::function const & pred) const { +format local_context::pp(formatter const & fmt, std::function const & pred) const { // NOLINT options const & opts = fmt.get_options(); unsigned indent = get_pp_indent(opts); unsigned max_hs = get_pp_goal_max_hyps(opts); diff --git a/src/library/local_context.h b/src/library/local_context.h index 0977b40d0b..0f686e1a1c 100644 --- a/src/library/local_context.h +++ b/src/library/local_context.h @@ -177,7 +177,7 @@ public: That is, all local_decl references in \c e are defined in this context. */ bool well_formed(expr const & e) const; - format pp(formatter const & fmt, std::function const & pred) const; + format pp(formatter const & fmt, std::function const & pred) const; // NOLINT format pp(formatter const & fmt) const { return pp(fmt, [](local_decl const &) { return true; }); } /** \brief Replaced assigned metavariables with their values.