From 778e8845b63186c06eb78bd495bb6d4b4726f0f8 Mon Sep 17 00:00:00 2001 From: Son Ho Date: Wed, 19 Jan 2022 21:44:38 +0100 Subject: Make minor modifications --- src/InterpreterBorrows.ml | 5 ++--- 1 file 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) -- cgit v1.2.3