diff --git a/src/frontends/lean/elaborator.cpp b/src/frontends/lean/elaborator.cpp
index b1fb2f6ff..41e46ad0c 100644
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@@ -126,22 +126,13 @@ optional<expr> elaborator::mvar_to_meta(expr const & mvar) {
         return none_expr();
 }
 
-static bool is_tactic_type(expr const & e) {
-    expr const * it = &e;
-    while (is_pi(*it)) {
-        it = &binding_body(*it);
-    }
-    return *it == get_tactic_type() || *it == get_tactic_expr_type() || *it == get_tactic_expr_list_type();
-}
-
 /** \brief Store the pair (pos(e), type(r)) in the info_data if m_info_manager is available. */
 void elaborator::save_type_data(expr const & e, expr const & r) {
     if (!m_no_info && infom() && pip() &&
         (is_constant(e) || is_local(e) || is_placeholder(e) || is_as_atomic(e) || is_consume_args(e))) {
         if (auto p = pip()->get_pos_info(e)) {
             expr t = m_tc[m_relax_main_opaque]->infer(r).first;
-            if (!is_tactic_type(t))
-                m_pre_info_data.add_type_info(p->first, p->second, t);
+            m_pre_info_data.add_type_info(p->first, p->second, t);
         }
     }
 }
@@ -160,8 +151,7 @@ void elaborator::save_extra_type_data(expr const & e, expr const & r) {
     if (!m_no_info && infom() && pip()) {
         if (auto p = pip()->get_pos_info(e)) {
             expr t = m_tc[m_relax_main_opaque]->infer(r).first;
-            if (!is_tactic_type(t))
-                m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
+            m_pre_info_data.add_extra_type_info(p->first, p->second, r, t);
         }
     }
 }
diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp
index 8d77cd067..15cacf38d 100644
--- a/src/frontends/lean/info_manager.cpp
+++ b/src/frontends/lean/info_manager.cpp
@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "library/choice.h"
 #include "library/scoped_ext.h"
 #include "library/tactic/proof_state.h"
+#include "library/tactic/expr_to_tactic.h"
 #include "frontends/lean/info_manager.h"
 #include "frontends/lean/pp_options.h"
 
@@ -351,7 +352,17 @@ struct info_manager::imp {
         m_env_info.insert(env_info(l, m_iteration, env, o));
     }
 
+    static bool is_tactic_type(expr const & e) {
+        expr const * it = &e;
+        while (is_pi(*it)) {
+            it = &binding_body(*it);
+        }
+        return *it == get_tactic_type() || *it == get_tactic_expr_type() || *it == get_tactic_expr_list_type();
+    }
+
     void add_type_info(unsigned l, unsigned c, expr const & e) {
+        if (is_tactic_type(e))
+            return;
         lock_guard<mutex> lc(m_mutex);
         if (m_block_new_info)
             return;
@@ -360,6 +371,8 @@ struct info_manager::imp {
     }
 
     void add_extra_type_info(unsigned l, unsigned c, expr const & e, expr const & t) {
+        if (is_tactic_type(t))
+            return;
         lock_guard<mutex> lc(m_mutex);
         if (m_block_new_info)
             return;