diff --git a/src/frontends/lean/decl_cmds.cpp b/src/frontends/lean/decl_cmds.cpp
index 67815078a..656c7e043 100644
--- a/src/frontends/lean/decl_cmds.cpp
+++ b/src/frontends/lean/decl_cmds.cpp
@@ -30,6 +30,11 @@ Author: Leonardo de Moura
 #include "frontends/lean/update_environment_exception.h"
 #include "frontends/lean/nested_declaration.h"
 
+// We don't display profiling information for declarations that take less than 0.01 secs
+#ifndef LEAN_PROFILE_THRESHOLD
+#define LEAN_PROFILE_THRESHOLD 0.01
+#endif
+
 namespace lean {
 static environment declare_universe(parser & p, environment env, name const & n, bool local) {
     if (local) {
@@ -799,7 +804,7 @@ class definition_cmd_fn {
             std::ostringstream msg;
             display_pos(msg);
             msg << " type checking time for " << m_name;
-            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str());
+            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
             return ::lean::check(m_env, d);
         } else {
             return ::lean::check(m_env, d);
@@ -955,7 +960,7 @@ class definition_cmd_fn {
             std::ostringstream msg;
             display_pos(msg);
             msg << " type elaboration time for " << m_name;
-            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str());
+            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
             return m_p.elaborate_type(e, list<expr>(), clear_pre_info);
         } else {
             return m_p.elaborate_type(e, list<expr>(), clear_pre_info);
@@ -968,7 +973,7 @@ class definition_cmd_fn {
             std::ostringstream msg;
             display_pos(msg);
             msg << " elaboration time for " << m_name;
-            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str());
+            timeit timer(m_p.diagnostic_stream().get_stream(), msg.str().c_str(), LEAN_PROFILE_THRESHOLD);
             return m_p.elaborate_definition(def_name, type, value);
         } else {
             return m_p.elaborate_definition(def_name, type, value);
diff --git a/src/util/timeit.h b/src/util/timeit.h
index 2cb88fd6f..8829a0a5c 100644
--- a/src/util/timeit.h
+++ b/src/util/timeit.h
@@ -11,20 +11,23 @@ Author: Leonardo de Moura
 #include <iomanip>
 
 namespace lean {
-/**
-   \brief Low tech timer for used for testing.
-*/
+/** \brief Low tech timer for used for testing. */
 class timeit {
     std::ostream & m_out;
     std::string    m_msg;
+    double         m_threshold; // we only display the result if time > m_threshold
     clock_t        m_start;
 public:
-    timeit(std::ostream & out, char const * msg):m_out(out), m_msg(msg) {
+    timeit(std::ostream & out, char const * msg, double threshold):m_out(out), m_msg(msg), m_threshold(threshold) {
         m_start = clock();
     }
+    timeit(std::ostream & out, char const * msg):timeit(out, msg, -0.1) {}
     ~timeit() {
         clock_t end = clock();
-        m_out << m_msg << " " << std::fixed << std::setprecision(5) << ((static_cast<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC) << " secs\n";
+        double result = ((static_cast<double>(end) - static_cast<double>(m_start)) / CLOCKS_PER_SEC);
+        if (result > m_threshold) {
+            m_out << m_msg << " " << std::fixed << std::setprecision(5) << result << " secs\n";
+        }
     }
 };
 }