diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 66a94e0da26cd239cc151f782597323caccaacfa..a150166d10efd01b75d088fb3656ce7456324988 100644
--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -267,7 +267,5 @@ Section code.
     iApply type_jump; solve_typing.
   Qed.
 
-  (* TODO:
-     Should we do try_lock?
-   *)
+  (* TODO: Should we do try_lock? *)
 End code.
diff --git a/theories/typing/lib/rwlock/rwlockwriteguard.v b/theories/typing/lib/rwlock/rwlockwriteguard.v
index 400022088ee7966bcb1b2c3af170eb8f8a20020f..985ed87d42590bd44f17182cc64fed589e64b2d4 100644
--- a/theories/typing/lib/rwlock/rwlockwriteguard.v
+++ b/theories/typing/lib/rwlock/rwlockwriteguard.v
@@ -116,7 +116,7 @@ Section rwlockwriteguard.
     eqtype E L (rwlockwriteguard α1 ty1) (rwlockwriteguard α2 ty2).
   Proof. intros. by eapply rwlockwriteguard_proper. Qed.
 
-  (* TODO: In Rust, the read guard is Sync if ty is Send+Sync. *)
+  (* TODO: In Rust, the write guard is Sync if ty is Send+Sync. *)
 End rwlockwriteguard.
 
 Hint Resolve rwlockwriteguard_mono' rwlockwriteguard_proper' : lrust_typing.