From bcdc3592aa0d3b866f9ae6e1875fdd6ef78f0887 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Mon, 22 Nov 2021 11:39:34 +0100
Subject: Make a minor modification in Interpreter.ml

---
 src/Interpreter.ml | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

(limited to 'src')

diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index 16089b86..3e5d7144 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -270,8 +270,5 @@ let rec end_borrow (config : config) (l : BorrowId.id) (env0 : env) : env =
       end_borrow config l env'
   (* If found mut: give the value back *)
   | FoundMut tv, env -> give_back_value config l tv env
-  (* If found shared: remove the borrow id from the loan set of the shared value *)
-  | FoundShared, env -> give_back_shared config l env
-  | FoundInactivatedMut, _env ->
-      (* We found an inactivated mut: activate it *)
-      unimplemented __LOC__
+  (* If found shared or inactivated mut: remove the borrow id from the loan set of the shared value *)
+  | (FoundShared | FoundInactivatedMut), env -> give_back_shared config l env
-- 
cgit v1.2.3