refine comments even more

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).

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.

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.