TODO.

TODO

@@ -44,12 +44,11 @@ and possibly the various kinds of environments that we use.
 
 Document the precondition and postcondition of every function.
 
-Deal with more complex forms of binding.
-  How do we deal with forms where a name can have several binding occurrences?
-  e.g., or-patterns, join-calculus
-  let, let rec, multiple let, multiple let rec, telescopes
-  What about the distinction between expression types and pattern types?
-  Term mode versus pattern mode in Unbound.
+------------------------------------------------------------------------------
+
+TODO (POSSIBLY):
+
+Change all of the macros to build objects on the fly instead of using classes?
 
 Try dealing with binding and hash-consing at the same time.
 
@@ -57,13 +56,3 @@ Try dealing with suspended substitutions.
   (As a distinct construct. Not necessarily at abstractions.)
 
 Look at the visitors in Why3.
-
-------------------------------------------------------------------------------
-
-TODO (POSSIBLY):
-
-Change all of the macros to build objects on the fly instead of using classes?
-
-Avoid reduce, which is not tail recursive.
-  Use iter in [ba] and [fa].
-  That should save a constant factor in stack usage?