From d3cfd392789256175abd4000a274cbaf05fbe0df Mon Sep 17 00:00:00 2001
From: Daniel Selsam <daniel.selsam@gmail.com>
Date: Sun, 3 Jul 2016 02:50:32 +0100
Subject: [PATCH] chore(tactic/simplifier/simplifier): remove old todos

---
 src/library/tactic/simplifier/simplifier.cpp | 2 --
 1 file changed, 2 deletions(-)

diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp
index acd34130c3..3b3f24c370 100644
--- a/src/library/tactic/simplifier/simplifier.cpp
+++ b/src/library/tactic/simplifier/simplifier.cpp
@@ -463,12 +463,10 @@ simp_result simplifier::simplify_extensions(expr const & _e) {
             } else {
                 lean_trace(name({"simplifier", "extensions"}),
                            tout() << "extension succeeded but left metavariables unassigned\n";);
-                // TODO(dhs): trace "simplifier.extension.failure"
             }
         } else {
             lean_trace(name({"simplifier", "extensions"}),
                        tout() << "extension failed\n";);
-            // TODO(dhs): trace "simplifier.extension.failure"
         }
     }
     return r;