diff --git a/src/library/app_builder.cpp b/src/library/app_builder.cpp index 796a01ccf5..f6660d6a7a 100644 --- a/src/library/app_builder.cpp +++ b/src/library/app_builder.cpp @@ -602,7 +602,7 @@ struct app_builder::imp { void trace_inst_failure(expr const & A, char const * n) { lean_trace("app_builder", - tout() << "failed to build instance of '" << n << "' for:\n" << A << "\n";); + tout() << "failed to build instance of '" << n << "' for " << A << "\n";); } expr mk_partial_add(expr const & A) { diff --git a/src/library/blast/blast.cpp b/src/library/blast/blast.cpp index a82b162821..dd85947317 100644 --- a/src/library/blast/blast.cpp +++ b/src/library/blast/blast.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "kernel/type_checker.h" #include "library/replace_visitor.h" #include "library/util.h" +#include "library/trace.h" #include "library/reducible.h" #include "library/class.h" #include "library/constants.h" @@ -1147,6 +1148,10 @@ optional blast_goal(environment const & env, io_state const & ios, list