diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index 7f21214d3a..bc181b271e 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -2297,6 +2297,9 @@ void elaborator::show_goal(tactic_state const & s, expr const & start_ref, expr
 /* Apply the given tactic to the state 's'.
    Report any errors detected during the process using position information associated with 'ref'. */
 tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const & s, expr const & ref) {
+    pos_info_provider * provider = get_pos_info_provider();
+    flycheck_output_scope flycheck(provider, ref);
+
     /* Compile tactic into bytecode */
     name tactic_name("_tactic");
     expr tactic_type = mk_tactic_unit();
@@ -2318,7 +2321,6 @@ tactic_state elaborator::execute_tactic(expr const & tactic, tactic_state const
         format fmt          = std::get<0>(*ex);
         optional<expr> ref1 = std::get<1>(*ex);
         tactic_state s1     = std::get<2>(*ex);
-        pos_info_provider * provider = get_pos_info_provider();
         if (ref1 && provider && provider->get_pos_info(*ref1))
             throw elaborator_exception(*ref1, fmt);
         else
diff --git a/src/library/flycheck.cpp b/src/library/flycheck.cpp
index 3dfd495645..b08e049ed1 100644
--- a/src/library/flycheck.cpp
+++ b/src/library/flycheck.cpp
@@ -5,6 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "library/flycheck.h"
+#include "library/error_handling.h"
 
 namespace lean {
 flycheck_scope::flycheck_scope(std::ostream & out, options const & o, char const * kind):
@@ -15,4 +16,32 @@ flycheck_scope::flycheck_scope(std::ostream & out, options const & o, char const
 flycheck_scope::~flycheck_scope() {
     if (m_flycheck) m_out << "FLYCHECK_END" << std::endl;
 }
+flycheck_output_scope::flycheck_output_scope(io_state const & ios, char const * stream_name, pos_info const & pos) :
+        m_stream_name(stream_name), m_pos(pos),
+        m_out(ios.get_regular_stream()),
+        m_redirected_ios(ios),
+        m_scoped_ios(), m_buffer() {
+    if (ios.get_options().get_bool("flycheck", false)) {
+        m_buffer = std::shared_ptr<string_output_channel>(new string_output_channel);
+        m_redirected_ios.set_diagnostic_channel(m_buffer);
+        m_redirected_ios.set_regular_channel(m_buffer);
+        m_scoped_ios = std::unique_ptr<scope_global_ios>(new scope_global_ios(m_redirected_ios));
+        lean_assert(enabled());
+    }
+}
+flycheck_output_scope::flycheck_output_scope(pos_info_provider const * provider, expr const & ref) :
+    flycheck_output_scope(get_global_ios(),
+                          provider ? provider->get_file_name() : "unknown",
+                          provider ? provider->get_pos_info_or_some(ref) : pos_info(0, 0)) {}
+flycheck_output_scope::~flycheck_output_scope() {
+    if (enabled()) {
+        auto redirected_output = m_buffer->str();
+        if (!redirected_output.empty()) {
+            m_out << "FLYCHECK_BEGIN INFORMATION" << std::endl;
+            display_pos(m_out, m_stream_name, m_pos.first, m_pos.second);
+            m_out << " information:" << std::endl << redirected_output;
+            m_out << "FLYCHECK_END" << std::endl;
+        }
+    }
+}
 }
diff --git a/src/library/flycheck.h b/src/library/flycheck.h
index 0ca2e96cbb..a3e394652b 100644
--- a/src/library/flycheck.h
+++ b/src/library/flycheck.h
@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <iostream>
+#include "kernel/pos_info_provider.h"
 #include "util/sexpr/options.h"
 #include "library/io_state.h"
 
@@ -22,6 +23,21 @@ public:
     bool enabled() const { return m_flycheck; }
 };
 
+/** Redirects regular and diagnostic output streams of the global ios as flycheck informations. */
+class flycheck_output_scope {
+    char const *                           m_stream_name;
+    pos_info                               m_pos;
+    std::ostream &                         m_out;
+    io_state                               m_redirected_ios;
+    std::unique_ptr<scope_global_ios>      m_scoped_ios;
+    std::shared_ptr<string_output_channel> m_buffer;
+public:
+    flycheck_output_scope(io_state const & ios, char const * stream_name, pos_info const & pos);
+    flycheck_output_scope(pos_info_provider const * provider, expr const & ref);
+    ~flycheck_output_scope();
+    bool enabled() const { return static_cast<bool>(m_scoped_ios); }
+};
+
 struct flycheck_error : public flycheck_scope {
     flycheck_error(std::ostream & out, options const & o):flycheck_scope(out, o, "ERROR") {}
     flycheck_error(io_state const & ios):flycheck_scope(ios, "ERROR") {}