diff --git a/TODO b/TODO
index b3546054665af8e62e73ab4b65cf5c773a6ca3ec..b60e690eeca89b9ebbc5805255e5afeddf7cdfcb 100644
--- a/TODO
+++ b/TODO
@@ -1,3 +1,12 @@
+------------------------------------------------------------------------------
+
+TODO (REALLY):
+
+Relax ba so as to not require well-formedness?
+  Define wf separately, relying on ba_wf internally.
+Global uniqueness, or uniqueness along a branch?
+  Which wf criterion do we want?
+
 Implement avoid, which renames the bound names of a term so as to
 avoid a certain set of names.
 
@@ -11,33 +20,16 @@ Or, suppose I want to annotate every abstraction with the
 Can I easily do it?
 Need a map_reduce visitor?
 
-If TVar is a constructor of some type other than term
-  (e.g. value: one substitutes values for variables in terms)
-  then Toolbox must be adapted.
-
 Check that every module has an .mli file, except where that would be too heavy.
 The type (_, _) abstraction could be transparent, private, or opaque.
 
-Benchmark fa versus fa' and decide which one to keep.
-
-Possibly cut Toolbox.Make down into several smaller functors.
-  At least [subst] should be a separate functor.
-
-Operations on terms:
-  simultaneous opening? (nominal)
-  conversion from debruijn back to nominal
-  a printer for debruijn terms?
-
--- test for global uniqueness everywhere an environment is extended?
-
 Operations on each kind of environment:
   Entering a binder (and testing for global uniqueness).
 
 Add printers for Atom.Map
 and possibly the various kinds of environments that we use.
 
-Document the precondition and postcondition of every function
-  in terms of ownership of atoms.
+Document the precondition and postcondition of every function.
 
 Deal with more complex forms of binding.
 
@@ -51,9 +43,3 @@ Look at the visitors in Why3.
 ------------------------------------------------------------------------------
 
 TODO (POSSIBLY):
-
-Can we treat 'bn specially so that we do not need to implement visit_'bn?
-  Or should we just mark 'bn as [@opaque] so as to get visit_'bn for free? Ugly.
-
-Operations in nominal style, without the GUH.
-  Capture-avoiding substitution with freshening of bound names.