diff --git a/src/todo.txt b/src/todo.txt
index a6b8544..e9e75ff 100644
--- a/src/todo.txt
+++ b/src/todo.txt
@@ -1,5 +1,7 @@
-- Add '--untyped' check for typeflaw detection (instead of the fairly
-  vague '--match'.
+- It is currently not well-defined to define inversekeys within a role:
+  this requires some work at instantiation, because instantiated term
+  couples should be added to the inverses list, and removed at
+  descruction.
 - Warshall is taking a third of the time running.
   - Make 'dirty' flag.
   - Make a push-graph structure, where old graphs are simply remembered?
@@ -28,8 +30,7 @@
   int termSymbolEqual(Term t1, Term t2);
   Iteration through the termlist should be done by hand.
 - Maybe add warning for type of matching in the output, maybe stderr.
+  Maybe all state-space bounding info should be displayed.
 - SConstruct file should check whether ctags actually exists (avoiding
   errors)
 - Proof output should be XML, with an external converter to dot format.
-- Internal hash over input files (maybe after parsing?) and switch
-  structure. This would make a caching mechanism much easier.