chore(frontends/lean/elaborator): fix outdated comment

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
2014-07-22 17:50:13 -07:00 · 2014-07-22 17:50:13 -07:00 · 90189f8eb6
commit 90189f8eb6
parent 35e7302d8a
1 changed files with 0 additions and 1 deletions
--- a/src/frontends/lean/elaborator.cpp
+++ b/src/frontends/lean/elaborator.cpp
@ -1018,7 +1018,6 @@ public:
            check_exact_tacs(pre_tac, subst);
            return some_expr(pre_tac);
        } else {
-            // TODO(Leo): m_env tactic hints
            return none_expr();
        }
    }