chore(simplifier): remove old TODO

2016-07-06 09:17:40 -07:00 · 2016-07-06 09:17:40 -07:00 · a354973fee
commit a354973fee
parent 10773760bc
1 changed files with 0 additions and 1 deletions
--- a/src/library/tactic/simplifier/simplifier.cpp
+++ b/src/library/tactic/simplifier/simplifier.cpp
@ -905,7 +905,6 @@ vm_obj tactic_simp_core(vm_obj const & rules, vm_obj const & prove_fn, vm_obj co
                name id;
                if (is_mlocal(rule)) id = mlocal_name(rule);
                else if (is_constant(rule)) id = const_name(rule);
-                // TODO(dhs): allow users to give priorities?
                lemmas = add(tctx, lemmas, id, tctx.infer(rule), rule, LEAN_DEFAULT_PRIORITY);
            });