Comments.

src/BindingForms.ml

@@ -33,20 +33,21 @@ type ('bn, 't, 'u) telescope =
    where the environment is enriched. *)
 
 (* These classes do not know the type of the environment, and do not know how
-   it is enriched; the latter task is delegated to virtual methods, such as
-   [extend] and [restrict]. The implementation of these methods is provided
-   by separate ``kits''. *)
+   it is enriched or looked up; the latter task is delegated to the virtual
+   methods [extend] and [lookup]. The implementation of these methods is
+   provided by separate ``kits''. *)
 
-(* We need one class per variety of visitor, which is a bit painful. *)
+(* We need several varieties of visitor, which is a bit painful. As of now,
+   [iter], [map], [endo], [iter2] are required: see [ToolboxInput]. *)
 
 (* The method [visit_abs] is polymorphic in the type of terms. This is
    important, as it means that one can use several instances of [abs] in a
    single type definition and still be able to construct well-typed
    visitors. *)
 
-(* The virtual methods [extend] and [restrict] are not polymorphic in the
-   types of bound names and environments. On the contrary, each kit comes
-   with certain specific types of bound names and environments. *)
+(* The virtual methods [extend] and [lookup] are not polymorphic in the types
+   of bound names and environments. On the contrary, each kit comes with
+   certain specific types of bound names and environments. *)
 
 (* -------------------------------------------------------------------------- *)