diff --git a/doc/todo.md b/doc/todo.md
index cc4a4184b8..788c7c019f 100644
--- a/doc/todo.md
+++ b/doc/todo.md
@@ -1,14 +1,7 @@
 To Do List
 ----------
 
-- Universe polymorphism.
-- Inductive datatypes.
-- New representation for metavariables.
-- New elaborator
-- Add unification hints support in the Lean front-end.
-- Improved extensible parser and pretty printer.
-- Notation-sets for organizing user defined notation.
+- Improved pretty printer.
 - Generic Tableaux prover.
 - [MCSat](http://leodemoura.github.io/files/fmcad2013.pdf) framework.
 - Independent type checker using a different programming language (e.g., F* or OCaml).
-- New apply-tactic.