Make minor cleaning

3 files changed, 10 insertions, 9 deletions

diff --git a/TODO.md b/TODO.md
index 3ee40513..2ca92016 100644
--- a/TODO.md
+++ b/TODO.md
@@ -1,5 +1,7 @@
 # TODO
 
+0. Update the high-level comments, in particular in Values.ml
+
 0. Rename Pure -> PureAst
 
 0. For variables pretty names: we could try to use the meta places used for the
diff --git a/src/Types.ml b/src/Types.ml
index 286b8163..4e9c69c8 100644
--- a/src/Types.ml
+++ b/src/Types.ml
@@ -31,11 +31,6 @@ type region_var = (RegionVarId.id, string option) indexed_var [@@deriving show]
     Regions are used in function signatures (in which case we use region variable
     ids) and in symbolic variables and projections (in which case we use region
     ids).
-    
-    TODO: use this only in the signatures. During interpretation, we need
-    a uniform treatment of regions as variables (otherwise the projectors
-    don't work: they always ignore the static regions...). By convention,
-    use region with id 0 as the static region.
  *)
 type 'rid region =
   | Static  (** Static region *)
@@ -177,13 +172,14 @@ type sty = RegionVarId.id gr_ty [@@deriving show, ord]
 type rty = RegionId.id gr_ty [@@deriving show, ord]
 (** Type with *R*egions.
 
-    Used during symbolic execution.
+    Used to project borrows/loans inside of abstractions, during symbolic
+    execution.
  *)
 
 type ety = erased_region ty [@@deriving show, ord]
 (** Type with *E*rased regions.
     
-    Used in function bodies, "general" value types, etc.
+    Used in function bodies, "regular" value types, etc.
  *)
 
 type field = { field_name : string; field_ty : sty } [@@deriving show]
@@ -200,7 +196,8 @@ type type_def = {
   type_params : type_var list;
   kind : type_def_kind;
   regions_hierarchy : region_var_groups;
-      (** Stored the hierarchy between the regions (which regions have the same lifetime,
-          what is the hierarchy between the lifetimes) *)
+      (** Stores the hierarchy between the regions (which regions have the
+          same lifetime, which lifetime should end before which other lifetime,
+          etc.) *)
 }
 [@@deriving show]
diff --git a/src/Values.ml b/src/Values.ml
index 25d354fb..f2807cfa 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -610,6 +610,8 @@ and aborrow_content =
           
           Note that we need to do so only for borrows consumed by parent
           abstractions (hence the optional borrow id).
+          
+          TODO: the below explanations are obsolete
 
           Example:
           ========