1 files changed, 5 insertions, 50 deletions

diff --git a/src/InterpreterBorrowsCore.ml b/src/InterpreterBorrowsCore.ml
index 455d62c3..8f6827b3 100644
--- a/src/InterpreterBorrowsCore.ml
+++ b/src/InterpreterBorrowsCore.ml
@@ -831,19 +831,18 @@ let remove_intersecting_aproj_borrows_shared (regions : T.RegionId.Set.t)
     Note that the new value [nv] with which to replace the proj_loans could
     be untyped: we request a typed value for sanity checking.
     
-    [subst]: takes as parameters the projection regions and the projection type
+    [subst]: takes as parameters the abstraction and the projection type
     where we perform the substitution.
  *)
 let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
     (proj_ty : T.rty) (sv : V.symbolic_value)
-    (subst : T.RegionId.Set.t -> T.rty -> V.aproj) (ctx : C.eval_ctx) :
-    C.eval_ctx =
+    (subst : V.abs -> T.rty -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
   (* Small helpers for sanity checks *)
   let updated = ref false in
-  let update local_regions local_proj_ty : V.aproj =
+  let update abs local_proj_ty : V.aproj =
     assert (not !updated);
     updated := true;
-    subst local_regions local_proj_ty
+    subst abs local_proj_ty
   in
   (* The visitor *)
   let obj =
@@ -864,7 +863,7 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
               if
                 projections_intersect proj_ty proj_regions sv'.V.sv_ty
                   abs.regions
-              then update abs.regions sv'.V.sv_ty
+              then update abs sv'.V.sv_ty
               else super#visit_aproj (Some abs) sproj)
             else super#visit_aproj (Some abs) sproj
     end
@@ -875,47 +874,3 @@ let update_intersecting_aproj_loans (proj_regions : T.RegionId.Set.t)
   assert !updated;
   (* Return *)
   ctx
-
-(*
-let proj_loans_intersect (proj_loans : T.RegionId.Set.t * V.symbolic_value)
-    (proj_loans' : T.RegionId.Set.t * V.symbolic_value) : bool =
-  let regions, sv = proj_loans in
-  let regions', sv' = proj_loans' in
-  if same_symbolic_id sv sv' then
-    projections_intersect sv.V.sv_ty regions sv'.V.sv_ty regions'
-  else false
-
-*)
-(*(** Substitute the proj_loans based an a symbolic id *)
-  let substitute_aproj_loans_with_id (sv : V.symbolic_value)
-      (subst : T.RegionId.Set.t -> V.aproj) (ctx : C.eval_ctx) : C.eval_ctx =
-    (* Small helpers for sanity checks *)
-    let updated = ref false in
-    let update regions : V.aproj =
-      updated := true;
-      subst regions
-    in
-    (* The visitor *)
-    let obj =
-      object
-        inherit [_] C.map_eval_ctx as super
-
-        method! visit_abs _ abs = super#visit_abs (Some abs) abs
-
-        method! visit_aproj abs sproj =
-          match sproj with
-          | AProjBorrows _ | AEndedProjLoans _ | AEndedProjBorrows
-          | AIgnoredProjBorrows ->
-              super#visit_aproj abs sproj
-          | AProjLoans sv' ->
-              let abs = Option.get abs in
-              if same_symbolic_id sv sv' then update abs.regions
-              else super#visit_aproj (Some abs) sproj
-      end
-    in
-    (* Apply *)
-    let ctx = obj#visit_eval_ctx None ctx in
-    (* Check that we updated the context at least once *)
-    assert !updated;
-    (* Return *)
-  ctx*)