diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index badd134390805e08c15665997d270e592e59f711..6c5b28aec2b72fd5d797c0f0eac4f87e0daf7142 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -175,7 +175,7 @@ Proof.
     f_equal; eauto using subst_is_closed_nil, is_closed_to_val, eq_sym.
 Qed.
 
-Definition atomic (e : expr) :=
+Definition is_atomic (e : expr) :=
   match e with
   | Alloc e => bool_decide (is_Some (to_val e))
   | Load e => bool_decide (is_Some (to_val e))
@@ -187,7 +187,7 @@ Definition atomic (e : expr) :=
   | App (Rec _ _ (Lit _)) (Lit _) => true
   | _ => false
   end.
-Lemma atomic_correct e : atomic e → language.atomic (to_expr e).
+Lemma is_atomic_correct e : is_atomic e → Atomic (to_expr e).
 Proof.
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *.
@@ -228,13 +228,11 @@ Hint Extern 10 (AsVal _) => solve_to_val : typeclass_instances.
 
 Ltac solve_atomic :=
   match goal with
-  | |- language.atomic ?e =>
-     let e' := W.of_expr e in change (language.atomic (W.to_expr e'));
-     apply W.atomic_correct; vm_compute; exact I
+  | |- Atomic ?e =>
+     let e' := W.of_expr e in change (Atomic (W.to_expr e'));
+     apply W.is_atomic_correct; vm_compute; exact I
   end.
-Hint Extern 10 (language.atomic _) => solve_atomic.
-(* For the side-condition of elim_upd_fupd_wp_atomic *)
-Hint Extern 10 (language.atomic _) => solve_atomic : typeclass_instances.
+Hint Extern 10 (Atomic _) => solve_atomic : typeclass_instances.
 
 (** Substitution *)
 Ltac simpl_subst :=
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 65da78ed1f05df4ba649a543d4b2d4b6a7910087..e9e92ab5ded233a35c1e720db1ae74327256c4a2 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -118,7 +118,7 @@ Section ectx_language.
   Lemma ectx_language_atomic e :
     (∀ σ e' σ' efs, head_step e σ e' σ' efs → irreducible e' σ') →
     sub_values e →
-    atomic e.
+    Atomic e.
   Proof.
     intros Hatomic_step Hatomic_fill σ e' σ' efs [K e1' e2' -> -> Hstep].
     assert (K = empty_ectx) as -> by eauto 10 using val_stuck.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index f465765b473d5b432cc5bc96614bb96f61ff5a48..cb110957a6880febd9f6dc2bdbc95021dedaac19 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -58,7 +58,7 @@ Proof.
 Qed.
 
 Lemma ht_atomic E1 E2 P P' Φ Φ' e :
-  atomic e →
+  Atomic e →
   (P ={E1,E2}=> P') ∧ {{ P' }} e @ E2 {{ Φ' }} ∧ (∀ v, Φ' v ={E2,E1}=> Φ v)
   ⊢ {{ P }} e @ E1 {{ Φ }}.
 Proof.
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index f2a9b9e8bb590682e803094e8d8e6af0f9d71ccb..8189151d5739006bfd683cd7dae9844bead6bf35 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -58,15 +58,15 @@ Section language.
      stronger sense defined below, and we have to be able to open invariants
      around that expression.  See `CasStuckS` in
      [lambdaRust](https://gitlab.mpi-sws.org/FP/LambdaRust-coq/blob/master/theories/lang/lang.v). *)
-  Definition atomic (e : expr Λ) : Prop :=
-    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → irreducible e' σ'.
+  Class Atomic (e : expr Λ) : Prop :=
+    atomic σ e' σ' efs : prim_step e σ e' σ' efs → irreducible e' σ'.
 
   (* To open invariants with a WP that does not ensure safety, we need a
      stronger form of atomicity.  With the above definition, in case `e` reduces
      to a stuck non-value, there is no proof that the invariants have been
      established again. *)
-  Definition strongly_atomic (e : expr Λ) : Prop :=
-    ∀ σ e' σ' efs, prim_step e σ e' σ' efs → is_Some (to_val e').
+  Class StronglyAtomic (e : expr Λ) : Prop :=
+    strongly_atomic σ e' σ' efs : prim_step e σ e' σ' efs → is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -87,9 +87,8 @@ Section language.
   Global Instance of_val_inj : Inj (=) (=) (@of_val Λ).
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
-  Lemma strongly_atomic_atomic e :
-    strongly_atomic e → atomic e.
-  Proof. unfold strongly_atomic, atomic. eauto using val_irreducible. Qed.
+  Lemma strongly_atomic_atomic e : StronglyAtomic e → Atomic e.
+  Proof. unfold StronglyAtomic, Atomic. eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
     to_val e = None → reducible (K e) σ → reducible e σ.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index e548668c04f1e2bbb649ec26228eabc86c801828..32b98d8ffa0e467c906d2cc02bf94778174cf49c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -147,7 +147,7 @@ Lemma wp_fupd E e Φ : WP e @ E {{ v, |={E}=> Φ v }} ⊢ WP e @ E {{ Φ }}.
 Proof. iIntros "H". iApply (wp_strong_mono E); try iFrame; auto. Qed.
 
 Lemma wp_atomic E1 E2 e Φ :
-  atomic e →
+  Atomic e →
   (|={E1,E2}=> WP e @ E2 {{ v, |={E2,E1}=> Φ v }}) ⊢ WP e @ E1 {{ Φ }}.
 Proof.
   iIntros (Hatomic) "H". rewrite !wp_unfold /wp_pre.
@@ -285,10 +285,8 @@ Section proofmode_classes.
 
   (* lower precedence, if possible, it should persistently pick elim_upd_fupd_wp *)
   Global Instance elim_modal_fupd_wp_atomic E1 E2 e P Φ :
-    atomic e →
+    Atomic e →
     ElimModal (|={E1,E2}=> P) P
             (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.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index 5fedc7f4cd2cf9a618b7c9d938dcbdbcd2920b3f..6834c5c5e3928fd626f706c6eda0a8daf90d433e 100644
--- a/theories/tests/ipm_paper.v
+++ b/theories/tests/ipm_paper.v
@@ -101,7 +101,7 @@ update modalities (which we did not cover in the paper). Normally we use these
 mask changing update modalities directly in our proofs, but in this file we use
 the first prove the rule as a lemma, and then use that. *)
 Lemma wp_inv_open `{irisG Λ Σ} N E P e Φ :
-  nclose N ⊆ E → atomic e →
+  nclose N ⊆ E → Atomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".