diff --git a/doc/todo.md b/doc/todo.md
index 62108bb41..ab07603cb 100644
--- a/doc/todo.md
+++ b/doc/todo.md
@@ -3,7 +3,7 @@ To Do List
 
 - ~~Add `cast : Pi (A B : Type) (H : A = B) (a : A) : B`, and implement "casting propagation" in the type checker.~~
 - ~~Modify the `let` construct to store the type of the value. The idea is to allow `let name : type := value in expr`. The type does not need to be provided by the user. However, the user may want to provide it as a hint for the Lean elaborator.~~
-- Refactor the elaborator code. The elaborator will be one of the main data-structures in Lean. The elaborator manager should be shared between different frontends.
+- ~~Refactor the elaborator code. The elaborator will be one of the main data-structures in Lean. The elaborator manager should be shared between different frontends.~~
 - ~~Reconsider whether meta-variables should be in `expr` or not. Metavariables (aka holes) are fundamental in our [design](design.md).~~
 - ~~Improve Lean pretty printer for Pi's. For example, it produces `Var a : Pi (A : Type) (_ : A), A` instead of `Var a : Pi (A : Type), A -> A`.~~
 - Decide what will be the main technique for customizing Lean's behavior. The elaborator manager will have many building blocks that can be put together in many different ways. Possible solutions: