From c27b98bd3d3575e33a0c6f345237071661f9f315 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 17 Jun 2021 12:40:45 +0200
Subject: [PATCH] comments in laterable.v

---
 iris/bi/lib/laterable.v | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/iris/bi/lib/laterable.v b/iris/bi/lib/laterable.v
index 968f678fb..0dee7157d 100644
--- a/iris/bi/lib/laterable.v
+++ b/iris/bi/lib/laterable.v
@@ -13,6 +13,9 @@ Global Hint Mode Laterable + ! : typeclass_instances.
     Well be the identity if [P] already is laterable, and add
     [make_laterable] otherwise. *)
 Class IntoLaterable {PROP : bi} (P Q : PROP) : Prop := {
+  (** This is non-standard; usually we would just demand
+      [P ⊢ make_laterable Q]. However, we need these stronger properties for
+      the [make_laterable_id] hack in [atomic.v]. *)
   into_laterable : P ⊢ Q;
   into_laterable_result_laterable : Laterable Q;
 }.
@@ -55,6 +58,10 @@ Section instances.
     iIntros "!> >_". done.
   Qed.
 
+  (** This instance, together with the one below, can lead to massive
+      backtracking, but only when searching for [Laterable]. In the future, it
+      should be rewritten using [Hint Immediate] or [Hint Cut], where the latter
+      is preferred once we figure out how to use it. *)
   Global Instance persistent_laterable `{!BiAffine PROP} P :
     Persistent P → Laterable P.
   Proof.
@@ -199,7 +206,11 @@ Section instances.
     - intros ?. done.
   Qed.
 
-  (** * Proofmode integration *)
+  (** * Proofmode integration
+
+      We integrate [make_laterable] with [iModIntro]. All non-laterable
+      hypotheses have a â–· added in front of them to ensure a laterable context.
+  *)
   Global Instance into_laterable_laterable P :
     Laterable P →
     IntoLaterable P P.
-- 
GitLab