From 66862a29cf023ca4d586479a9690dc4f61d8573c Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 21 Apr 2022 11:12:34 +0200
Subject: Work on pretty names

---
 src/InterpreterBorrows.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'src/InterpreterBorrows.ml')

diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 065a39b9..89dfb274 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1202,12 +1202,12 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
           ^ aborrow_content_to_string ctx bc));
       let ctx =
         match bc with
-        | V.AMutBorrow (mv, bid, av) ->
+        | V.AMutBorrow (_mv, bid, av) ->
             (* First, convert the avalue to a (fresh symbolic) value *)
             let sv = convert_avalue_to_given_back_value abs.kind av in
             (* Replace the mut borrow to register the fact that we ended
              * it and store with it the freshly generated given back value *)
-            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (mv, sv, av)) in
+            let ended_borrow = V.ABorrow (V.AEndedMutBorrow (sv, av)) in
             let ctx = update_aborrow ek_all bid ended_borrow ctx in
             (* Give the value back *)
             let sv = mk_typed_value_from_symbolic_value sv in
@@ -1256,9 +1256,7 @@ and end_abstraction_borrows (config : C.config) (chain : borrow_or_abs_ids)
       (* Generate a fresh symbolic value *)
       let nsv = mk_fresh_symbolic_value V.FunCallGivenBack proj_ty in
       (* Replace the proj_borrows - there should be exactly one *)
-      let ended_borrow =
-        V.AEndedProjBorrows { original = sv; given_back = nsv }
-      in
+      let ended_borrow = V.AEndedProjBorrows nsv in
       let ctx = update_aproj_borrows abs.abs_id sv ended_borrow ctx in
       (* Give back the symbolic value *)
       let ctx =
-- 
cgit v1.2.3