diff --git a/program_logic/weakestpre.v b/program_logic/weakestpre.v
index ffaa00fa5a3ab26c19a96439eec93cba7918dae5..59efd2377b8d71255686ed2a016e43d5c87f4bc5 100644
--- a/program_logic/weakestpre.v
+++ b/program_logic/weakestpre.v
@@ -314,3 +314,5 @@ Section proofmode_classes.
             (WP e @ E1 {{ Φ }}) (WP e @ E2 {{ v, |={E2,E1}=> Φ v }})%I | 100.
   Proof. intros. by rewrite /ElimModal fupd_frame_r wand_elim_r wp_atomic. Qed.
 End proofmode_classes.
+
+Hint Extern 0 (atomic _) => assumption : typeclass_instances.