summaryrefslogtreecommitdiff
path: root/src/SymbolicToPure.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/SymbolicToPure.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/SymbolicToPure.ml b/src/SymbolicToPure.ml
index 1985bfd3..80d08ac4 100644
--- a/src/SymbolicToPure.ml
+++ b/src/SymbolicToPure.ml
@@ -678,7 +678,7 @@ and aborrow_content_to_consumed (_ctx : bs_ctx) (bc : V.aborrow_content) :
| AEndedIgnoredMutBorrow _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
- | AProjSharedBorrow _ ->
+ | AEndedSharedBorrow | AProjSharedBorrow _ ->
(* Ignore *)
None
@@ -784,7 +784,7 @@ and aborrow_content_to_given_back (bc : V.aborrow_content) (ctx : bs_ctx) :
| AEndedIgnoredMutBorrow _ ->
(* This happens with nested borrows: we need to dive in *)
raise Unimplemented
- | AProjSharedBorrow _ ->
+ | AEndedSharedBorrow | AProjSharedBorrow _ ->
(* Ignore *)
(ctx, None)