From f2f98080a4531c2f4ac8c5cad53a71bcea2b9457 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 28 Apr 2017 16:47:33 +0200
Subject: [PATCH] refine comments even more

---
 theories/typing/lib/rwlock/rwlock.v           | 2 +-
 theories/typing/lib/rwlock/rwlockreadguard.v  | 1 +
 theories/typing/lib/rwlock/rwlockwriteguard.v | 1 +
 3 files changed, 3 insertions(+), 1 deletion(-)

diff --git a/theories/typing/lib/rwlock/rwlock.v b/theories/typing/lib/rwlock/rwlock.v
index a75c30b7..fd500488 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 1eb2b274..74bee0c8 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 04b3c8c4..22521426 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.
-- 
GitLab