From a354973fee591cea3679cd8cc3a3ad47f3b1075b Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Wed, 6 Jul 2016 09:17:40 -0700 Subject: [PATCH] chore(simplifier): remove old TODO --- src/library/tactic/simplifier/simplifier.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/library/tactic/simplifier/simplifier.cpp b/src/library/tactic/simplifier/simplifier.cpp index 375689baae..a398441ec8 100644 --- 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); });