diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 64ae740d5d6c08cb471aea913747e563423d5d79..1eb2b274e5a7125be007a32699c725d89e1ab044 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -119,9 +119,9 @@ Section rwlockreadguard.
     move=>?????/=. apply uPred.exist_mono=>?. by rewrite sync_change_tid.
   Qed.
 
-  (* Probably for reasons related to the underlying representation,
-     Rust does not implement Send for RwLockWriteGuard. We could prove
-     this. *)
+  (* POSIX requires the unlock to occur from the thread that acquired
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
+     prove this. *)
 End rwlockreadguard.
 
 Hint Resolve rwlockreadguard_mono' rwlockreadguard_proper' : lrust_typing.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index b439613c138162fa8879b04525246a3078f079a0..04b3c8c42ee1f3aef212a0a804b55cb6b294265e 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -123,9 +123,9 @@ Section rwlockwriteguard.
     by rewrite sync_change_tid.
   Qed.
 
-  (* Probably for reasons related to the underlying representation,
-     Rust does not implement Send for RwLockWriteGuard. We could prove
-     this. *)
+  (* POSIX requires the unlock to occur from the thread that acquired
+     the lock, so Rust does not implement Send for RwLockWriteGuard. We could
+     prove this. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.