From 6dc90d5f3f3f2bc367efc57c221a967c3937d66e Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Thu, 13 Nov 2014 00:13:12 +0100
Subject: [PATCH] TODO Update

---
 TODO.md | 7 -------
 1 file changed, 7 deletions(-)

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)?