diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/InterpreterBorrows.ml | 5 |
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) |