diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 6a8fd1de71f1300e7987a56cc1e45a6a188ae7c3..40d030f26ee3c1539905ce1d011de723b67f556b 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.