Make minor cleaning

2 files changed, 8 insertions, 9 deletions

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:
           ========