diff --git a/TODO.md b/TODO.md
index b98e03f4..0662d4e8 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,8 +1,12 @@
-# Main goals
+# Goals
 
-- Fonctorise solver.ml with term module and theory module
-- Add proof output
+- Functorise `solver.ml` with term module and theory module
+    * SAT solver depends on actual boolean literals
+    * Move terms and theories (SMT part) to another directory
+- Add proof output as resolution
+    * Each theory brings its own proof output (tautologies), somehow
+    * pure resolution proofs between boolean clauses and theory tautologies
+- 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)?
 
-# Subgoals
-
-- Move terms and theories to another directory (once fonctorised) ?