summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2022-01-19 21:44:38 +0100
committerSon Ho2022-01-19 21:44:38 +0100
commit778e8845b63186c06eb78bd495bb6d4b4726f0f8 (patch)
treee47e70146dee0bc51e88e9ea9a7b05064ff2aa11
parent516d691ff26d2a60bd5a97bd2a5cd769b86b154b (diff)
Make minor modifications
-rw-r--r--src/InterpreterBorrows.ml5
1 files changed, 2 insertions, 3 deletions
diff --git a/src/InterpreterBorrows.ml b/src/InterpreterBorrows.ml
index 9333d389..38447fd1 100644
--- a/src/InterpreterBorrows.ml
+++ b/src/InterpreterBorrows.ml
@@ -1457,13 +1457,12 @@ let rec activate_inactivated_mut_borrow (config : C.config) (l : V.BorrowId.id)
let cc = end_outer_borrows config bids in
(* Promote the loan *)
let cc = comp cc (promote_shared_loan_to_mut_loan l) in
- (* let ctx, borrowed_value = promote_shared_loan_to_mut_loan l ctx in *)
(* Promote the borrow - the value should have been checked by
[promote_shared_loan_to_mut_loan]
*)
let cc =
- comp cc (fun cf borrowed_value ctx ->
- promote_inactivated_borrow_to_mut_borrow l cf borrowed_value ctx)
+ comp cc (fun cf borrowed_value ->
+ promote_inactivated_borrow_to_mut_borrow l cf borrowed_value)
in
(* Continue *)
cc cf ctx)