From d5410b27c74b64d460415d9f730d3d9c003a38c3 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 11 Aug 2022 09:25:03 -0400
Subject: [PATCH] remove stale reference to Laterable

---
 iris_heap_lang/proofmode.v | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 6a8fd1de7..40d030f26 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -631,10 +631,9 @@ Tactic Notation "wp_smart_apply" open_constr(lem) :=
 
 (** Tactic tailored for atomic triples: the first, simple one just runs
 [iAuIntro] on the goal, as atomic triples always have an atomic update as their
-premise.  The second one additionaly does some framing: it gets rid of [Hs] from
-the context, which is intended to be the non-laterable assertions that iAuIntro
-would choke on.  You get them all back in the continuation of the atomic
-operation. *)
+premise. The second one additionaly does some framing: it gets rid of [Hs] from
+the context, reducing clutter. You get them all back in the continuation of the
+atomic operation. *)
 Tactic Notation "awp_apply" open_constr(lem) :=
   wp_apply_core lem ltac:(fun H => iApplyHyp H) ltac:(fun cont => fail);
   last iAuIntro.
-- 
GitLab