diff options
| author | Son Ho | 2021-11-22 11:39:34 +0100 |
|---|---|---|
| committer | Son Ho | 2021-11-22 11:39:34 +0100 |
| commit | bcdc3592aa0d3b866f9ae6e1875fdd6ef78f0887 (patch) | |
| tree | 98df62e639766b4127c04bf442253438f97567f1 | |
| parent | 3e6b1a77ecc94726c02533bf1bbb915c483a2107 (diff) | |
Make a minor modification in Interpreter.ml
| -rw-r--r-- | src/Interpreter.ml | 7 |
1 files changed, 2 insertions, 5 deletions
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 |