diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e081ea449dc7bd80198541916a14470d4064ab49..8c60346e2e6a1d97ff582d769f6b8f62f0762eb7 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -400,4 +400,3 @@ Section proofmode_classes.
             (WP e @ s; E1 {{ Φ }}) (WP e @ s; E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
-