From c88d6dd1286e2ba680cf2cc852d8ef0e77b97751 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 27 Apr 2017 15:36:04 +0200
Subject: [PATCH] TODO comments

---
 theories/typing/lib/mutex/mutexguard.v        | 4 +---
 theories/typing/lib/rwlock/rwlockwriteguard.v | 2 +-
 2 files changed, 2 insertions(+), 4 deletions(-)

diff --git a/theories/typing/lib/mutex/mutexguard.v b/theories/typing/lib/mutex/mutexguard.v
index 66a94e0d..a150166d 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 40002208..985ed87d 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.
-- 
GitLab