From cbff5ea8561b633c4c785fe3fa117025b593f84f Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 16 Aug 2013 17:28:52 -0700
Subject: [PATCH] Cleanup

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/exprlib/printer.cpp    | 4 ++++
 src/kernel/environment.cpp | 3 ---
 src/kernel/expr.cpp        | 3 ---
 src/kernel/expr.h          | 2 --
 src/kernel/free_vars.cpp   | 1 -
 src/kernel/instantiate.h   | 1 -
 src/kernel/type_check.cpp  | 2 --
 7 files changed, 4 insertions(+), 12 deletions(-)

diff --git a/src/exprlib/printer.cpp b/src/exprlib/printer.cpp
index de27c4764..08c4466e2 100644
--- a/src/exprlib/printer.cpp
+++ b/src/exprlib/printer.cpp
@@ -171,3 +171,7 @@ std::ostream & operator<<(std::ostream & out, environment const & env) {
     return out;
 }
 }
+void print(lean::expr const & a) { std::cout << a << std::endl; }
+void print(lean::expr const & a, lean::context const & c) { std::cout << mk_pair(a, c) << std::endl; }
+void print(lean::context const & c) { std::cout << c << std::endl; }
+void print(lean::environment const & e) { std::cout << e << std::endl; }
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index 0f6408da1..c1797926d 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -7,14 +7,11 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <atomic>
-#include <sstream>
 #include <unordered_map>
 #include "kernel_exception.h"
 #include "environment.h"
 #include "safe_arith.h"
 #include "type_check.h"
-#include "exception.h"
-#include "debug.h"
 
 namespace lean {
 
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index a78994296..0afd849a1 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -11,10 +11,8 @@ Author: Leonardo de Moura
 #include "free_vars.h"
 #include "expr_sets.h"
 #include "hash.h"
-#include "format.h"
 
 namespace lean {
-
 unsigned hash_args(unsigned size, expr const * args) {
     return hash(size, [&args](unsigned i){ return args[i].hash(); });
 }
@@ -204,4 +202,3 @@ expr copy(expr const & a) {
     return expr();
 }
 }
-void print(lean::expr const & a) { std::cout << a << "\n"; }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 98083119b..bcc721906 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -387,7 +387,6 @@ struct expr_cell_offset_eqp { unsigned operator()(expr_cell_offset const & p1, e
 
 // =======================================
 // Miscellaneous
-std::ostream & operator<<(std::ostream & out, expr const & a);
 /**
    \brief Wrapper for iterating over application arguments.
 
@@ -468,4 +467,3 @@ template<typename F> expr update_eq(expr const & e, F f) {
 }
 // =======================================
 }
-void print(lean::expr const & a);
diff --git a/src/kernel/free_vars.cpp b/src/kernel/free_vars.cpp
index fd51bedf1..f0c927e5a 100644
--- a/src/kernel/free_vars.cpp
+++ b/src/kernel/free_vars.cpp
@@ -186,5 +186,4 @@ expr lift_free_vars(expr const & e, unsigned d) {
     };
     return replace_fn<decltype(f)>(f)(e);
 }
-
 }
diff --git a/src/kernel/instantiate.h b/src/kernel/instantiate.h
index 42bc21e90..1f1694810 100644
--- a/src/kernel/instantiate.h
+++ b/src/kernel/instantiate.h
@@ -21,5 +21,4 @@ inline expr instantiate_with_closed(expr const & e, expr const & s) { return ins
 */
 expr instantiate(expr const & e, unsigned n, expr const * s);
 inline expr instantiate(expr const & e, expr const & s) { return instantiate(e, 1, &s); }
-
 }
diff --git a/src/kernel/type_check.cpp b/src/kernel/type_check.cpp
index 6dd4d1a59..6884bf4cd 100644
--- a/src/kernel/type_check.cpp
+++ b/src/kernel/type_check.cpp
@@ -12,7 +12,6 @@ Author: Leonardo de Moura
 #include "scoped_map.h"
 #include "builtin.h"
 #include "free_vars.h"
-#include "trace.h"
 
 namespace lean {
 bool is_convertible_core(expr const & expected, expr const & given, environment const & env) {
@@ -58,7 +57,6 @@ struct infer_type_fn {
     }
 
     level infer_universe(expr const & t, context const & ctx) {
-        lean_trace("type_check", tout << "infer universe\n" << t << "\n";);
         expr u = normalize(infer_type(t, ctx), m_env, ctx);
         if (is_type(u))
             return ty_level(u);