summaryrefslogtreecommitdiff
path: root/src/Print.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-26 10:04:52 +0100
committerSon Ho2022-01-26 10:04:52 +0100
commit14833cb33792703bf87c7e7d933687f289886294 (patch)
treeb7c18f894854372dbd318f9b5dd3b6c54696aa7e /src/Print.ml
parent144b660f7cfb8b65672f5872c05272a9caa0de78 (diff)
Add a meta-value in SharedBorrow to carry the shared value
Diffstat (limited to 'src/Print.ml')
-rw-r--r--src/Print.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Print.ml b/src/Print.ml
index cefa3ea5..da6158b5 100644
--- a/src/Print.ml
+++ b/src/Print.ml
@@ -278,7 +278,7 @@ module Values = struct
and borrow_content_to_string (fmt : value_formatter) (bc : V.borrow_content) :
string =
match bc with
- | SharedBorrow bid -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
+ | SharedBorrow (_, bid) -> "⌊shared@" ^ V.BorrowId.to_string bid ^ "⌋"
| MutBorrow (bid, tv) ->
"&mut@" ^ V.BorrowId.to_string bid ^ " ("
^ typed_value_to_string fmt tv