summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorSon Ho2021-12-07 18:07:01 +0100
committerSon Ho2021-12-07 18:07:01 +0100
commitbef8563b4429785df6c0c63e75ca5c6631ed4687 (patch)
treea441e117be8376dcb997c08f1ff6327ac21b340b
parent9b9c54e7c2dc5a2e77f34efa890d87f4292ba070 (diff)
Make a minor modification
Diffstat (limited to '')
-rw-r--r--src/Interpreter.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Interpreter.ml b/src/Interpreter.ml
index fc95e136..f371e84f 100644
--- a/src/Interpreter.ml
+++ b/src/Interpreter.ml
@@ -226,7 +226,7 @@ let lookup_borrow_opt (ek : exploration_kind) (l : V.BorrowId.id) (env : C.env)
if bid = l then raise (FoundBorrowContent (V.MutBorrow (bid, mv)))
else if ek.enter_mut_borrows then super#visit_MutBorrow env bid mv
else ()
- (** Check the borrow id and control diving *)
+ (** Check the borrow id and control the diving *)
method! visit_SharedBorrow env bid =
if bid = l then raise (FoundBorrowContent (V.SharedBorrow bid)) else ()