From ea3fae060fe5906f46338fc17fc2d224edb6851c Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 2 May 2016 18:18:53 -0700 Subject: [PATCH] chore(compiler/preprocess_rec): use tout --- src/compiler/preprocess_rec.cpp | 11 ++++------- 1 file changed, 4 insertions(+), 7 deletions(-) diff --git a/src/compiler/preprocess_rec.cpp b/src/compiler/preprocess_rec.cpp index c7c4097a51..c1cbe67686 100644 --- a/src/compiler/preprocess_rec.cpp +++ b/src/compiler/preprocess_rec.cpp @@ -7,6 +7,7 @@ Author: Leonardo de Moura #include "kernel/declaration.h" #include "kernel/type_checker.h" #include "kernel/instantiate.h" +#include "library/trace.h" #include "library/aux_recursors.h" #include "library/user_recursors.h" #include "library/util.h" @@ -17,9 +18,6 @@ Author: Leonardo de Moura #include "compiler/inliner.h" #include "compiler/lambda_lifting.h" -void pp_detail(lean::environment const & env, lean::expr const & e); -void pp(lean::environment const & env, lean::expr const & e); - namespace lean { class expand_aux_recursors_fn : public compiler_step_visitor { bool is_aux_recursor(expr const & e) { @@ -67,12 +65,11 @@ class preprocess_rec_fn { void display(expr const & v) { for (name const & n : m_aux_decls) { - std::cout << ">> " << n << "\n"; + tout() << ">> " << n << "\n"; declaration d = m_env.get(n); - ::pp_detail(m_env, d.get_value()); + tout() << d.get_value() << "\n"; } - std::cout << ">> main\n"; - ::pp_detail(m_env, v); + tout() << ">> main\n" << v << "\n"; } public: