diff options
author | Son Ho | 2022-12-02 08:59:41 +0100 |
---|---|---|
committer | Son HO | 2023-02-03 11:21:46 +0100 |
commit | 175949360a0208d826be89463c916fbaaa7fa8a4 (patch) | |
tree | c650b9c2340115522cbea55cebb015e2110e92c4 /compiler/SymbolicToPure.ml | |
parent | b2a494f8fc3acdf1cfab7b4d6d10b1bd316663f8 (diff) |
Remove the meta-value field from AMutBorrow
Diffstat (limited to '')
-rw-r--r-- | compiler/SymbolicToPure.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/compiler/SymbolicToPure.ml b/compiler/SymbolicToPure.ml index 81cc22e1..6c956fe8 100644 --- a/compiler/SymbolicToPure.ml +++ b/compiler/SymbolicToPure.ml @@ -949,7 +949,7 @@ and aloan_content_to_consumed (ctx : bs_ctx) (ectx : C.eval_ctx) and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) : texpression option = match bc with - | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> raise (Failure "Unreachable") | AEndedMutBorrow (_, _) -> (* We collect consumed values: ignore *) @@ -1089,7 +1089,7 @@ and aloan_content_to_given_back (_mp : mplace option) (lc : V.aloan_content) and aborrow_content_to_given_back (mp : mplace option) (bc : V.aborrow_content) (ctx : bs_ctx) : bs_ctx * typed_pattern option = match bc with - | V.AMutBorrow (_, _, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> + | V.AMutBorrow (_, _) | ASharedBorrow _ | AIgnoredMutBorrow (_, _) -> raise (Failure "Unreachable") | AEndedMutBorrow (msv, _) -> (* Return the meta-symbolic-value *) |