diff --git a/TODO.md b/TODO.md
index 8e9836c1..019ddf7e 100644
--- a/TODO.md
+++ b/TODO.md
@@ -2,13 +2,6 @@
 
 ## Main goals
 
-- Modify theories to allow passing bulk of assumed literals
-    * Create shared "vector" (formulas/atoms ?)
-    * Allow theory propagation
-- Cleanup code
-    * Simplify Solver.Make functor
-- Add proof output for smt/theories
-    * Each theory brings its own proof output (tautologies), somehow
 - Allow to plug one's code into boolean propagation
     * react upon propagation (possibly by propagating more, or side-effect)
     * more advanced/specific propagation (2-clauses)?