diff --git a/theories/logatom/rdcss/rdcss.v b/theories/logatom/rdcss/rdcss.v
index 4aa1066234c0154cfebe66fdee0b655efd47d0b7..27a30a516a49ecc868b8a1ce4252c944a0578b7e 100644
--- a/theories/logatom/rdcss/rdcss.v
+++ b/theories/logatom/rdcss/rdcss.v
@@ -387,7 +387,8 @@ Section rdcss.
       (* FIXME: proof duplication *)
       wp_apply (wp_resolve with "Hp"); first done. wp_cmpxchg_fail.
       iIntros (vs'' ->) "Hp". iModIntro.
-      iSplitL "Done Hp". { by eauto 12 with iFrame. } iModIntro.
+      iSplitL "Done Hp". { by eauto 12 with iFrame. }
+      iModIntro.
       iSplitL "Hln Hrest". { by eauto 12 with iFrame. }
       wp_seq. iApply "HQ".
       iApply state_done_extract_Q; done.