Introduce AEndedSharedBorrow so as not to introduce ABottom when

ending shared aborrows

1 files changed, 4 insertions, 0 deletions

diff --git a/src/Values.ml b/src/Values.ml
index 57d188da..25d354fb 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -681,6 +681,10 @@ and aborrow_content =
           in practice the child value should only contain ended borrows, ignored
           values, bottom values, etc.
        *)
+  | AEndedSharedBorrow
+      (** We don't really need [AEndedSharedBorrow]: we simply want to be
+          precise, and not insert ⊥ when ending borrows.
+       *)
   | AEndedIgnoredMutBorrow of {
       child : typed_avalue;
       given_back_loans_proj : typed_avalue;