diff --git a/src/library/tactic/simplify.cpp b/src/library/tactic/simplify.cpp
index f6808b744b..156746d0e8 100644
--- a/src/library/tactic/simplify.cpp
+++ b/src/library/tactic/simplify.cpp
@@ -17,6 +17,7 @@ Author: Daniel Selsam, Leonardo de Moura
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
 #include "library/trace.h"
+#include "library/annotation.h"
 #include "library/pp_options.h"
 #include "library/constants.h"
 #include "library/normalize.h"
@@ -726,9 +727,11 @@ simp_result simplify_core_fn::visit(expr const & e, optional<expr> const & paren
         case expr_kind::Meta:
         case expr_kind::Sort:
         case expr_kind::Constant:
-        case expr_kind::Macro:
             new_result = curr_result;
             break;
+        case expr_kind::Macro:
+            new_result = join(curr_result, visit_macro(curr_result.get_new()));
+            break;
         case expr_kind::Var:
             lean_unreachable();
         case expr_kind::Lambda:
@@ -1059,6 +1062,14 @@ simp_result simplify_ext_core_fn::visit_pi(expr const & e) {
     return simplify_core_fn::visit_pi(e);
 }
 
+simp_result simplify_ext_core_fn::visit_macro(expr const & e) {
+    if (is_annotation(e)) {
+        return visit(get_annotation_arg(e), none_expr());
+    } else {
+        return simplify_core_fn::visit_macro(e);
+    }
+}
+
 simp_result simplify_ext_core_fn::visit_let(expr const & e) {
     /* TODO(Leo): when m_zeta is false, we need to implement efficient code for checking whether the abstraction of
        a let-body is type correct or not */
diff --git a/src/library/tactic/simplify.h b/src/library/tactic/simplify.h
index d36e05919f..29d2f29421 100644
--- a/src/library/tactic/simplify.h
+++ b/src/library/tactic/simplify.h
@@ -145,6 +145,7 @@ protected:
     virtual simp_result visit_lambda(expr const & e) override;
     virtual simp_result visit_pi(expr const & e) override;
     virtual simp_result visit_let(expr const & e) override;
+    virtual simp_result visit_macro(expr const & e) override;
 public:
     simplify_ext_core_fn(type_context & ctx, defeq_canonizer::state & dcs, simp_lemmas const & slss,
                          simp_config const & cfg);