From 0841a63dcefc0b8adf00b22c20542c4c8d8fdc68 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 7 Dec 2017 15:29:02 +0100
Subject: [PATCH] CamlCase of inductive constructors

---
 CHANGELOG.md                           | 10 +++++-----
 theories/heap_lang/tactics.v           |  2 +-
 theories/program_logic/adequacy.v      |  8 ++++----
 theories/program_logic/ectx_language.v |  2 +-
 theories/program_logic/hoare.v         | 16 ++++++++--------
 theories/program_logic/language.v      | 10 +++++-----
 theories/program_logic/lifting.v       |  8 ++++----
 theories/program_logic/ownp.v          | 14 +++++++-------
 theories/program_logic/weakestpre.v    | 25 +++++++++++++------------
 theories/tests/heap_lang.v             |  2 +-
 theories/tests/ipm_paper.v             |  2 +-
 11 files changed, 50 insertions(+), 49 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index b06ef6950..f969fd8ee 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 fc056d5ba..dafbf9824 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 1b325d981..6192bd377 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 5763c56f0..25a241279 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 89aea2a78..23857734d 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 28d47f037..26f813c5f 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 e64d685a5..f1299cee6 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 ffb599ad8..abd3aa7da 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 0525de9e6..677f071d7 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 829e5d3be..2d91879aa 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 c9d41b148..38ad33dc6 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]".
-- 
GitLab