doc(todo): update todo

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

doc/todo.md

@@ -1,19 +1,14 @@
 To Do List
 ----------
 
-- Finish Sigma-type support.
+- Universe polymorphism.
-- Build Nat and List theories.
+- Inductive datatypes.
-- Fix usability issues identified when formalizing optional and sum types.
+- New representation for metavariables.
+- New elaborator
 - Add unification hints support in the Lean front-end.
-- Improve simp tactic interface (more configuration options).
+- Improved extensible parser and pretty printer.
-- Add ssreflect-like rewrite commands.
+- Notation-sets for organizing user defined notation.
-- Add record-type (as syntax sugar for Sigma-types).
-- Implement inductive datatypes and recursive function package from first principles. The goal is to use the HOL/Isabelle approach.
 - 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).
-- Module for reading [OpenTheory](http://www.gilith.com/research/opentheory/) proofs.
+- New apply-tactic.
-- Re-implement apply-tactic.
-- Improve performance of `is_convertible` and `is_definitionally_equal` predicates.
-- Create notation sets. We are currently puting all notation decls in a "single bag".
-- Improve macro support, and allow users to provide arbitrary parser extensions using Lua.