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