summaryrefslogtreecommitdiff
path: root/src/Values.ml
diff options
context:
space:
mode:
authorSon Ho2022-01-12 14:23:10 +0100
committerSon Ho2022-01-12 14:23:10 +0100
commitce333b8591d7fd856aa16d54c0a0abbc8983fc63 (patch)
treebe53b580473030a8da8622005560cfcd7adc74b6 /src/Values.ml
parentf2dd12e889cca6e75b03868a7d31952c8bdfa9c7 (diff)
Make minor modifications
Diffstat (limited to 'src/Values.ml')
-rw-r--r--src/Values.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Values.ml b/src/Values.ml
index bcb08dc8..e8d4560e 100644
--- a/src/Values.ml
+++ b/src/Values.ml
@@ -422,7 +422,7 @@ and aborrow_content =
> x -> shared_loan {l0} (U32 0)
> px -> ⊥
- > abs0 { a_shared_bororw l0 }
+ > abs0 { a_shared_borrow l0 }
```
*)
| AIgnoredMutBorrow of BorrowId.id option * typed_avalue