diff --git a/iris_heap_lang/proofmode.v b/iris_heap_lang/proofmode.v
index 8826570fa48047f6ec29d893c13bcba692daa9f1..46b122bfe78b39e854bf3728c25c5b21e15bb07e 100644
--- a/iris_heap_lang/proofmode.v
+++ b/iris_heap_lang/proofmode.v
@@ -86,7 +86,8 @@ Tactic Notation "wp_pure" open_constr(efoc) :=
       unify e' efoc;
       eapply (tac_wp_pure _ _ _ _ K e');
       [iSolveTC                       (* PureExec *)
-      |try solve_vals_compare_safe    (* The pure condition for PureExec -- handles trivial goals, including [vals_compare_safe] *)
+      |try solve_vals_compare_safe    (* The pure condition for PureExec --
+         handles trivial goals, including [vals_compare_safe] *)
       |iSolveTC                       (* IntoLaters *)
       |wp_finish                      (* new goal *)
       ])