diff --git a/CHANGELOG.md b/CHANGELOG.md
index b06ef6950cbe9f28675d04f2a3fa9d7525b0c282..f969fd8eeb91d79b2f175347fddb451d908a20f2 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -20,7 +20,7 @@ Changes in and extensions of the theory:
   }}` ensures that, as usual, all invariants are preserved while `e` runs, but
   it permits execution to get stuck. The former implies the latter. The full
   judgment is `WP e @ s; E {{ Φ }}`, where non-stuck WP uses *stuckness bit* `s
-  = not_stuck` while stuck WP uses `s = maybe_stuck`.
+  = NotStuck` while stuck WP uses `s = MaybeStuck`.
 
 Changes in Coq:
 
@@ -105,10 +105,10 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret
 * Move the `prelude` folder to its own project: std++
 * The rules `internal_eq_rewrite` and `internal_eq_rewrite_contractive` are now
   stated in the logic, i.e. they are `iApply` friendly.
-* Restore the original, stronger notion of atomicity alongside the
-  weaker notion. These are `Atomic s e` where the stuckness bit `s`
-  indicates whether expression `e` is weakly (`s = not_stuck`) or
-  strongly (`s = maybe_stuck`) atomic.
+* Restore the original, stronger notion of atomicity alongside the weaker
+  notion. These are `Atomic a e` where the stuckness bit `s` indicates whether
+  expression `e` is weakly (`a = WeaklyAtomic`) or strongly (`a =
+  StronglyAtomic`) atomic.
 
 ## Iris 3.0.0 (released 2017-01-11)
 
diff --git a/theories/heap_lang/tactics.v b/theories/heap_lang/tactics.v
index fc056d5ba0a0eea6f003d44447a31c2104815c5c..dafbf982451ae2f881ce5294ea15c543e5e1da83 100644
--- a/theories/heap_lang/tactics.v
+++ b/theories/heap_lang/tactics.v
@@ -189,7 +189,7 @@ Definition is_atomic (e : expr) :=
   end.
 Lemma is_atomic_correct s e : is_atomic e → Atomic s (to_expr e).
 Proof.
-  enough (is_atomic e → Atomic strongly_atomic (to_expr e)).
+  enough (is_atomic e → Atomic StronglyAtomic (to_expr e)).
   { destruct s; auto using strongly_atomic_atomic. }
   intros He. apply ectx_language_atomic.
   - intros σ e' σ' ef Hstep; simpl in *. revert Hstep.
diff --git a/theories/program_logic/adequacy.v b/theories/program_logic/adequacy.v
index 1b325d9811ce40f10b85c43c00ee24fdc84e1a7b..6192bd377000010addebb5ccdf7fbf5cc6489a8c 100644
--- a/theories/program_logic/adequacy.v
+++ b/theories/program_logic/adequacy.v
@@ -38,20 +38,20 @@ Record adequate {Λ} (s : stuckness) (e1 : expr Λ) (σ1 : state Λ) (φ : val 
   adequate_result t2 σ2 v2 :
    rtc step ([e1], σ1) (of_val v2 :: t2, σ2) → φ v2;
   adequate_safe t2 σ2 e2 :
-   s = not_stuck →
+   s = NotStuck →
    rtc step ([e1], σ1) (t2, σ2) →
    e2 ∈ t2 → (is_Some (to_val e2) ∨ reducible e2 σ2)
 }.
 
 Theorem adequate_tp_safe {Λ} (e1 : expr Λ) t2 σ1 σ2 φ :
-  adequate not_stuck e1 σ1 φ →
+  adequate NotStuck e1 σ1 φ →
   rtc step ([e1], σ1) (t2, σ2) →
   Forall (λ e, is_Some (to_val e)) t2 ∨ ∃ t3 σ3, step (t2, σ2) (t3, σ3).
 Proof.
   intros Had ?.
   destruct (decide (Forall (λ e, is_Some (to_val e)) t2)) as [|Ht2]; [by left|].
   apply (not_Forall_Exists _), Exists_exists in Ht2; destruct Ht2 as (e2&?&He2).
-  destruct (adequate_safe not_stuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
+  destruct (adequate_safe NotStuck e1 σ1 φ Had t2 σ2 e2) as [?|(e3&σ3&efs&?)];
     rewrite ?eq_None_not_Some; auto.
   { exfalso. eauto. }
   destruct (elem_of_list_split t2 e2) as (t2'&t2''&->); auto.
@@ -144,7 +144,7 @@ Qed.
 
 Lemma wptp_safe n e1 e2 t1 t2 σ1 σ2 Φ :
   nsteps step n (e1 :: t1, σ1) (t2, σ2) → e2 ∈ t2 →
-  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp not_stuck t1
+  world σ1 ∗ WP e1 {{ Φ }} ∗ wptp NotStuck t1
   ⊢ ▷^(S (S n)) ⌜is_Some (to_val e2) ∨ reducible e2 σ2⌝.
 Proof.
   intros ? He2. rewrite wptp_steps // laterN_later. apply: bupd_iter_laterN_mono.
diff --git a/theories/program_logic/ectx_language.v b/theories/program_logic/ectx_language.v
index 5763c56f0399cf969855deec9db9ea6e92ddf07b..25a2412795b3c11d821ebb0a93a4d443b6caba93 100644
--- a/theories/program_logic/ectx_language.v
+++ b/theories/program_logic/ectx_language.v
@@ -132,7 +132,7 @@ Section ectx_language.
   Definition head_atomic (a : atomicity) (e : expr Λ) : Prop :=
     ∀ σ e' σ' efs,
       head_step e σ e' σ' efs →
-      if a is weakly_atomic then irreducible e' σ' else is_Some (to_val e').
+      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
   (* Some lemmas about this language *)
   Lemma fill_not_val K e : to_val e = None → to_val (fill K e) = None.
diff --git a/theories/program_logic/hoare.v b/theories/program_logic/hoare.v
index 89aea2a78eb24aea1cdd701062b751d09bfeffdd..23857734d46f7caf190cbed7db95704390d4ad7e 100644
--- a/theories/program_logic/hoare.v
+++ b/theories/program_logic/hoare.v
@@ -11,32 +11,32 @@ Instance: Params (@ht) 5.
 Notation "{{ P } } e @ s ; E {{ Φ } }" := (ht s E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  s ;  E  {{  Φ  } }") : stdpp_scope.
-Notation "{{ P } } e @ E {{ Φ } }" := (ht not_stuck E P%I e%E Φ%I)
+Notation "{{ P } } e @ E {{ Φ } }" := (ht NotStuck E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  {{  Φ  } }") : stdpp_scope.
-Notation "{{ P } } e @ E ? {{ Φ } }" := (ht maybe_stuck E P%I e%E Φ%I)
+Notation "{{ P } } e @ E ? {{ Φ } }" := (ht MaybeStuck E P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  @  E  ? {{  Φ  } }") : stdpp_scope.
-Notation "{{ P } } e {{ Φ } }" := (ht not_stuck ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e {{ Φ } }" := (ht NotStuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  {{  Φ  } }") : stdpp_scope.
-Notation "{{ P } } e ? {{ Φ } }" := (ht maybe_stuck ⊤ P%I e%E Φ%I)
+Notation "{{ P } } e ? {{ Φ } }" := (ht MaybeStuck ⊤ P%I e%E Φ%I)
   (at level 20, P, e, Φ at level 200,
    format "{{  P  } }  e  ? {{  Φ  } }") : stdpp_scope.
 
 Notation "{{ P } } e @ s ; E {{ v , Q } }" := (ht s E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  s ;  E  {{  v ,  Q  } }") : stdpp_scope.
-Notation "{{ P } } e @ E {{ v , Q } }" := (ht not_stuck E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E {{ v , Q } }" := (ht NotStuck E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  {{  v ,  Q  } }") : stdpp_scope.
-Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht maybe_stuck E P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e @ E ? {{ v , Q } }" := (ht MaybeStuck E P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  @  E  ? {{  v ,  Q  } }") : stdpp_scope.
-Notation "{{ P } } e {{ v , Q } }" := (ht not_stuck ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e {{ v , Q } }" := (ht NotStuck ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  {{  v ,  Q  } }") : stdpp_scope.
-Notation "{{ P } } e ? {{ v , Q } }" := (ht maybe_stuck ⊤ P%I e%E (λ v, Q)%I)
+Notation "{{ P } } e ? {{ v , Q } }" := (ht MaybeStuck ⊤ P%I e%E (λ v, Q)%I)
   (at level 20, P, e, Q at level 200,
    format "{{  P  } }  e  ? {{  v ,  Q  } }") : stdpp_scope.
 
diff --git a/theories/program_logic/language.v b/theories/program_logic/language.v
index 28d47f037b05a1165b4fc19cb89cb9e9f6b60a3d..26f813c5f55797ec836638ee85968fa61eb58554 100644
--- a/theories/program_logic/language.v
+++ b/theories/program_logic/language.v
@@ -53,7 +53,7 @@ Class LanguageCtx {Λ : language} (K : expr Λ → expr Λ) := {
 Instance language_ctx_id Λ : LanguageCtx (@id (expr Λ)).
 Proof. constructor; naive_solver. Qed.
 
-Inductive atomicity := strongly_atomic | weakly_atomic.
+Inductive atomicity := StronglyAtomic | WeaklyAtomic.
 
 Section language.
   Context {Λ : language}.
@@ -74,21 +74,21 @@ Section language.
   Definition stuck (e : expr Λ) (σ : state Λ) :=
     to_val e = None ∧ irreducible e σ.
 
-  (* [Atomic weakly_atomic]: This (weak) form of atomicity is enough to open
+  (* [Atomic WeaklyAtomic]: This (weak) form of atomicity is enough to open
      invariants when WP ensures safety, i.e., programs never can get stuck.  We
      have an example in lambdaRust of an expression that is atomic in this
      sense, but not in the 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).
 
-     [Atomic strongly_atomic]: To open invariants with a WP that does not ensure
+     [Atomic StronglyAtomic]: 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. *)
   Class Atomic (a : atomicity) (e : expr Λ) : Prop :=
     atomic σ e' σ' efs :
       prim_step e σ e' σ' efs →
-      if a is weakly_atomic then irreducible e' σ' else is_Some (to_val e').
+      if a is WeaklyAtomic then irreducible e' σ' else is_Some (to_val e').
 
   Inductive step (ρ1 ρ2 : cfg Λ) : Prop :=
     | step_atomic e1 σ1 e2 σ2 efs t1 t2 :
@@ -110,7 +110,7 @@ Section language.
   Proof. by intros v v' Hv; apply (inj Some); rewrite -!to_of_val Hv. Qed.
 
   Lemma strongly_atomic_atomic e :
-    Atomic strongly_atomic e → Atomic weakly_atomic e.
+    Atomic StronglyAtomic e → Atomic WeaklyAtomic e.
   Proof. unfold Atomic. eauto using val_irreducible. Qed.
 
   Lemma reducible_fill `{LanguageCtx Λ K} e σ :
diff --git a/theories/program_logic/lifting.v b/theories/program_logic/lifting.v
index e64d685a5a94e3b79ef58fe141d908d01dd5b020..f1299cee628ffbf79759ea943f47c145bc1576d4 100644
--- a/theories/program_logic/lifting.v
+++ b/theories/program_logic/lifting.v
@@ -15,7 +15,7 @@ Implicit Types Φ : val Λ → iProp Σ.
 Lemma wp_lift_step s E Φ e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E,∅}=∗
-    ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
       state_interp σ2 ∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
@@ -36,7 +36,7 @@ Qed.
 
 (** Derived lifting lemmas. *)
 Lemma wp_lift_pure_step `{Inhabited (state Λ)} s E E' Φ e1 :
-  (∀ σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
   (|={E,E'}▷=> ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
     WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -69,7 +69,7 @@ Qed.
 Lemma wp_lift_atomic_step {s E Φ} e1 :
   to_val e1 = None →
   (∀ σ1, state_interp σ1 ={E}=∗
-    ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
+    ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
     ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={E}=∗
       state_interp σ2 ∗
       default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -85,7 +85,7 @@ Proof.
 Qed.
 
 Lemma wp_lift_pure_det_step `{Inhabited (state Λ)} {s E E' Φ} e1 e2 efs :
-  (∀ σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+  (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
   (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
   (|={E,E'}▷=> WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
   ⊢ WP e1 @ s; E {{ Φ }}.
diff --git a/theories/program_logic/ownp.v b/theories/program_logic/ownp.v
index ffb599ad8be42135b8babef18535ba0d2f1d12cc..abd3aa7da9fcff5683e152cf3facf8b9f26a2530 100644
--- a/theories/program_logic/ownp.v
+++ b/theories/program_logic/ownp.v
@@ -86,7 +86,7 @@ Section lifting.
   Proof. rewrite /ownP; apply _. Qed.
 
   Lemma ownP_lift_step s E Φ e1 :
-    (|={E,∅}=> ∃ σ1, ⌜if s is not_stuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 ∗
+    (|={E,∅}=> ∃ σ1, ⌜if s is NotStuck then reducible e1 σ1 else to_val e1 = None⌝ ∗ ▷ ownP σ1 ∗
       ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2
             ={∅,E}=∗ WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -119,7 +119,7 @@ Section lifting.
   Qed.
 
   Lemma ownP_lift_pure_step `{Inhabited (state Λ)} s E Φ e1 :
-    (∀ σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ σ1 e2 σ2 efs, prim_step e1 σ1 e2 σ2 efs → σ1 = σ2) →
     (▷ ∀ e2 efs σ, ⌜prim_step e1 σ e2 σ efs⌝ →
       WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
@@ -136,7 +136,7 @@ Section lifting.
 
   (** Derived lifting lemmas. *)
   Lemma ownP_lift_atomic_step {s E Φ} e1 σ1 :
-    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (▷ ownP σ1 ∗ ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ -∗ ownP σ2 -∗
       default False (to_val e2) Φ ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤ {{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -151,7 +151,7 @@ Section lifting.
   Qed.
 
   Lemma ownP_lift_atomic_det_step {s E Φ e1} σ1 v2 σ2 efs :
-    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
                      σ2 = σ2' ∧ to_val e2' = Some v2 ∧ efs = efs') →
     ▷ ownP σ1 ∗ ▷ (ownP σ2 -∗
@@ -164,7 +164,7 @@ Section lifting.
   Qed.
 
   Lemma ownP_lift_atomic_det_step_no_fork {s E e1} σ1 v2 σ2 :
-    (if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ e2' σ2' efs', prim_step e1 σ1 e2' σ2' efs' →
       σ2 = σ2' ∧ to_val e2' = Some v2 ∧ [] = efs') →
     {{{ ▷ ownP σ1 }}} e1 @ s; E {{{ RET v2; ownP σ2 }}}.
@@ -174,7 +174,7 @@ Section lifting.
   Qed.
 
   Lemma ownP_lift_pure_det_step `{Inhabited (state Λ)} {s E Φ} e1 e2 efs :
-    (∀ σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ efs = efs')→
     ▷ (WP e2 @ s; E {{ Φ }} ∗ [∗ list] ef ∈ efs, WP ef @ s; ⊤{{ _, True }})
     ⊢ WP e1 @ s; E {{ Φ }}.
@@ -184,7 +184,7 @@ Section lifting.
   Qed.
 
   Lemma ownP_lift_pure_det_step_no_fork `{Inhabited (state Λ)} {s E Φ} e1 e2 :
-    (∀ σ1, if s is not_stuck then reducible e1 σ1 else to_val e1 = None) →
+    (∀ σ1, if s is NotStuck then reducible e1 σ1 else to_val e1 = None) →
     (∀ σ1 e2' σ2 efs', prim_step e1 σ1 e2' σ2 efs' → σ1 = σ2 ∧ e2 = e2' ∧ [] = efs') →
     ▷ WP e2 @ s; E {{ Φ }} ⊢ WP e1 @ s; E {{ Φ }}.
   Proof.
diff --git a/theories/program_logic/weakestpre.v b/theories/program_logic/weakestpre.v
index 0525de9e6db84c18308b86dc11d05173eabf165b..677f071d729775ae8f35c0521e86e57fd6cff52c 100644
--- a/theories/program_logic/weakestpre.v
+++ b/theories/program_logic/weakestpre.v
@@ -11,11 +11,11 @@ Class irisG' (Λstate : Type) (Σ : gFunctors) := IrisG {
 }.
 Notation irisG Λ Σ := (irisG' (state Λ) Σ).
 
-Inductive stuckness := not_stuck | maybe_stuck.
+Inductive stuckness := NotStuck | MaybeStuck.
 
 Definition stuckness_le (s1 s2 : stuckness) : bool :=
   match s1, s2 with
-  | maybe_stuck, not_stuck => false
+  | MaybeStuck, NotStuck => false
   | _, _ => true
   end.
 Instance: PreOrder stuckness_le.
@@ -25,7 +25,7 @@ Qed.
 Instance: SqSubsetEq stuckness := stuckness_le.
 
 Definition stuckness_to_atomicity (s : stuckness) : atomicity :=
-  if s is maybe_stuck then strongly_atomic else weakly_atomic.
+  if s is MaybeStuck then StronglyAtomic else WeaklyAtomic.
 
 Definition wp_pre `{irisG Λ Σ} (s : stuckness)
     (wp : coPset -c> expr Λ -c> (val Λ -c> iProp Σ) -c> iProp Σ) :
@@ -33,7 +33,7 @@ Definition wp_pre `{irisG Λ Σ} (s : stuckness)
   match to_val e1 with
   | Some v => |={E}=> Φ v
   | None => ∀ σ1,
-     state_interp σ1 ={E,∅}=∗ ⌜if s is not_stuck then reducible e1 σ1 else True⌝ ∗
+     state_interp σ1 ={E,∅}=∗ ⌜if s is NotStuck then reducible e1 σ1 else True⌝ ∗
      ▷ ∀ e2 σ2 efs, ⌜prim_step e1 σ1 e2 σ2 efs⌝ ={∅,E}=∗
        state_interp σ2 ∗ wp E e2 Φ ∗
        [∗ list] ef ∈ efs, wp ⊤ ef (λ _, True)
@@ -57,32 +57,32 @@ Instance: Params (@wp) 6.
 Notation "'WP' e @ s ; E {{ Φ } }" := (wp s E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  s ;  E  {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e @ E {{ Φ } }" := (wp not_stuck E e%E Φ)
+Notation "'WP' e @ E {{ Φ } }" := (wp NotStuck E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e @ E ? {{ Φ } }" := (wp maybe_stuck E e%E Φ)
+Notation "'WP' e @ E ? {{ Φ } }" := (wp MaybeStuck E e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' @  E  ? {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e {{ Φ } }" := (wp not_stuck ⊤ e%E Φ)
+Notation "'WP' e {{ Φ } }" := (wp NotStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' {{  Φ  } } ']'") : uPred_scope.
-Notation "'WP' e ? {{ Φ } }" := (wp maybe_stuck ⊤ e%E Φ)
+Notation "'WP' e ? {{ Φ } }" := (wp MaybeStuck ⊤ e%E Φ)
   (at level 20, e, Φ at level 200,
    format "'[' 'WP'  e  '/' ? {{  Φ  } } ']'") : uPred_scope.
 
 Notation "'WP' e @ s ; E {{ v , Q } }" := (wp s E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  s ;  E  {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e @ E {{ v , Q } }" := (wp not_stuck E e%E (λ v, Q))
+Notation "'WP' e @ E {{ v , Q } }" := (wp NotStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  E  {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e @ E ? {{ v , Q } }" := (wp maybe_stuck E e%E (λ v, Q))
+Notation "'WP' e @ E ? {{ v , Q } }" := (wp MaybeStuck E e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' @  E  ? {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e {{ v , Q } }" := (wp not_stuck ⊤ e%E (λ v, Q))
+Notation "'WP' e {{ v , Q } }" := (wp NotStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' {{  v ,  Q  } } ']'") : uPred_scope.
-Notation "'WP' e ? {{ v , Q } }" := (wp maybe_stuck ⊤ e%E (λ v, Q))
+Notation "'WP' e ? {{ v , Q } }" := (wp MaybeStuck ⊤ e%E (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'WP'  e  '/' ? {{  v ,  Q  } } ']'") : uPred_scope.
 
@@ -400,3 +400,4 @@ 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.
+
diff --git a/theories/tests/heap_lang.v b/theories/tests/heap_lang.v
index 829e5d3be7248d0f229aee1986b11de2e6e71d21..2d91879aaf71fdedcef9c1ccacd04f866e95d9f2 100644
--- a/theories/tests/heap_lang.v
+++ b/theories/tests/heap_lang.v
@@ -96,5 +96,5 @@ Section LiftingTests.
   Proof. iIntros "". wp_apply Pred_spec. wp_let. by wp_apply Pred_spec. Qed.
 End LiftingTests.
 
-Lemma heap_e_adequate σ : adequate not_stuck heap_e σ (= #2).
+Lemma heap_e_adequate σ : adequate NotStuck heap_e σ (= #2).
 Proof. eapply (heap_adequacy heapΣ)=> ?. by apply heap_e_spec. Qed.
diff --git a/theories/tests/ipm_paper.v b/theories/tests/ipm_paper.v
index c9d41b1485f584db4db4fe9094aaac64f94eaaa9..38ad33dc6008a9b944c4cbde62ae79efa1be00d9 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 weakly_atomic e →
+  nclose N ⊆ E → Atomic WeaklyAtomic e →
   inv N P ∗ (▷ P -∗ WP e @ E ∖ ↑N {{ v, ▷ P ∗ Φ v }}) ⊢ WP e @ E {{ Φ }}.
 Proof.
   iIntros (??) "[#Hinv Hwp]".