diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index a75c30b74c9169d2ee33bcb6955d4539396e96d0..fd50048884df235bd6da87541ac13336fcb9314f 100644
--- a/theories/typing/lib/rwlock/rwlock.v
+++ b/theories/typing/lib/rwlock/rwlock.v
@@ -189,7 +189,7 @@ Section rwlock.
     eqtype E L ty1 ty2 → eqtype E L (rwlock ty1) (rwlock ty2).
   Proof. eapply rwlock_proper. Qed.
 
-  (* TODO : apparently, we don't need to require ty to be sync,
+  (* Apparently, we don't need to require ty to be sync,
      contrarily to Rust's implementation. *)
   Global Instance rwlock_send :
     Send ty → Send (rwlock ty).
diff --git a/theories/typing/lib/rwlock/rwlockreadguard.v b/theories/typing/lib/rwlock/rwlockreadguard.v
index 1eb2b274e5a7125be007a32699c725d89e1ab044..74bee0c89473610dbbb460cab90c34f33ce81a32 100644
--- a/theories/typing/lib/rwlock/rwlockreadguard.v
+++ b/theories/typing/lib/rwlock/rwlockreadguard.v
@@ -113,6 +113,7 @@ Section rwlockreadguard.
     eqtype E L (rwlockreadguard α1 ty1) (rwlockreadguard α2 ty2).
   Proof. intros. by eapply rwlockreadguard_proper. Qed.
 
+  (* Rust requires the type to also be Send.  Not sure why. *)
   Global Instance rwlockreadguard_sync α ty :
     Sync ty → Sync (rwlockreadguard α ty).
   Proof.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 04b3c8c42ee1f3aef212a0a804b55cb6b294265e..22521426d9a8ac787bca9c8b1ec804199e07316f 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -116,6 +116,7 @@ Section rwlockwriteguard.
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
 
+  (* Rust requires the type to also be Send.  Not sure why. *)
   Global Instance rwlockwriteguard_sync α ty :
     Sync ty → Sync (rwlockwriteguard α ty).
   Proof.