diff --git a/iris/model.v b/iris/model.v
index 77dbb5612fc69a3fef412915ccfeafe61bf7c765..61b2f1566a4e73bd0e7bead9e68a045f1fc45004 100644
--- a/iris/model.v
+++ b/iris/model.v
@@ -24,7 +24,9 @@ End iProp.
 Definition iPreProp (Σ : iParam) : cofeT := iProp.result Σ.
 Notation iRes Σ := (res Σ (laterC (iPreProp Σ))).
 Notation iResRA Σ := (resRA Σ (laterC (iPreProp Σ))).
-Notation iCMRA Σ := (icmra Σ (laterC (iPreProp Σ))).
+Notation iWld Σ := (mapRA positive (agreeRA (laterC (iPreProp Σ)))).
+Notation iPst Σ := (exclRA (istateC Σ)).
+Notation iGst Σ := (icmra Σ (laterC (iPreProp Σ))).
 Definition iProp (Σ : iParam) : cofeT := uPredC (iResRA Σ).
 Definition iProp_unfold {Σ} : iProp Σ -n> iPreProp Σ := solution_fold _.
 Definition iProp_fold {Σ} : iPreProp Σ -n> iProp Σ := solution_unfold _.
@@ -38,3 +40,7 @@ Instance iProp_fold_inj n Σ : Injective (dist n) (dist n) (@iProp_fold Σ).
 Proof. by intros X Y H; rewrite -(iProp_unfold_fold X) H iProp_unfold_fold. Qed.
 Instance iProp_unfold_inj n Σ : Injective (dist n) (dist n) (@iProp_unfold Σ).
 Proof. by intros X Y H; rewrite -(iProp_fold_unfold X) H iProp_fold_unfold. Qed.
+
+Module Test. (* Make sure we got the notations right. *)
+  Definition iResTest (Σ : iParam) (w : iWld Σ) (p : iPst Σ) (g : iGst Σ) : iRes Σ := Res w p g.
+End Test.
diff --git a/iris/ownership.v b/iris/ownership.v
index 48103aebc7863d8d26706df7544160386d1fafde..68f99ad9ed2a43029f8a4c980358cfcac86a168f 100644
--- a/iris/ownership.v
+++ b/iris/ownership.v
@@ -4,7 +4,7 @@ Definition inv {Σ} (i : positive) (P : iProp Σ) : iProp Σ :=
   uPred_own (Res {[ i ↦ to_agree (Later (iProp_unfold P)) ]} ∅ ∅).
 Arguments inv {_} _ _%I.
 Definition ownP {Σ} (σ : istate Σ) : iProp Σ := uPred_own (Res ∅ (Excl σ) ∅).
-Definition ownG {Σ} (m : iCMRA Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
+Definition ownG {Σ} (m : iGst Σ) : iProp Σ := uPred_own (Res ∅ ∅ m).
 Instance: Params (@inv) 2.
 Instance: Params (@ownP) 1.
 Instance: Params (@ownG) 1.
@@ -16,7 +16,7 @@ Context {Σ : iParam}.
 Implicit Types r : iRes Σ.
 Implicit Types σ : istate Σ.
 Implicit Types P : iProp Σ.
-Implicit Types m : iCMRA Σ.
+Implicit Types m : iGst Σ.
 
 (* Invariants *)
 Global Instance inv_contractive i : Contractive (@inv Σ i).
diff --git a/iris/pviewshifts.v b/iris/pviewshifts.v
index 3ce4f29fe4b4d22fa979a240212b67dbd0260af8..81ee2f4eec368916dff1dd9f5a644d6597aa6a31 100644
--- a/iris/pviewshifts.v
+++ b/iris/pviewshifts.v
@@ -29,7 +29,7 @@ Instance: Params (@pvs) 3.
 Section pvs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : iCMRA Σ.
+Implicit Types m : iGst Σ.
 Transparent uPred_holds.
 
 Global Instance pvs_ne E1 E2 n : Proper (dist n ==> dist n) (@pvs Σ E1 E2).
@@ -96,7 +96,7 @@ Proof.
   * by rewrite -(left_id_L ∅ (∪) Ef).
   * apply uPred_weaken with r n; auto.
 Qed.
-Lemma pvs_updateP E m (P : iCMRA Σ → Prop) :
+Lemma pvs_updateP E m (P : iGst Σ → Prop) :
   m ⇝: P → ownG m ⊑ pvs E E (∃ m', ■ P m' ∧ ownG m').
 Proof.
   intros Hup r [|n] ? Hinv%ownG_spec rf [|k] Ef σ ???; try lia.
diff --git a/iris/viewshifts.v b/iris/viewshifts.v
index 4c3da218a3c8fa4a20566185aae85edb396d3e6b..a090f5f85fe5109f780a1947396385de47d7de59 100644
--- a/iris/viewshifts.v
+++ b/iris/viewshifts.v
@@ -16,7 +16,7 @@ Notation "P >{ E }> Q" := (True ⊑ vs E E P%I Q%I)
 Section vs.
 Context {Σ : iParam}.
 Implicit Types P Q : iProp Σ.
-Implicit Types m : iCMRA Σ.
+Implicit Types m : iGst Σ.
 Import uPred.
 
 Lemma vs_alt E1 E2 P Q : P ⊑ pvs E1 E2 Q → P >{E1,E2}> Q.
@@ -85,7 +85,7 @@ Proof.
   intros; rewrite -{1}(left_id_L ∅ (∪) E) -vs_mask_frame; last solve_elem_of.
   apply vs_close.
 Qed.
-Lemma vs_updateP E m (P : iCMRA Σ → Prop) :
+Lemma vs_updateP E m (P : iGst Σ → Prop) :
   m ⇝: P → ownG m >{E}> (∃ m', ■ P m' ∧ ownG m').
 Proof. by intros; apply vs_alt, pvs_updateP. Qed.
 Lemma vs_update E m m' : m ⇝ m' → ownG m >{E}> ownG m'.
diff --git a/iris/wsat.v b/iris/wsat.v
index 3f197c2d76195de5b5606564e5a27418960dcd05..a9afb6facf148e02209c15dbb595ae259154af8f 100644
--- a/iris/wsat.v
+++ b/iris/wsat.v
@@ -120,7 +120,7 @@ Proof.
   split; [done|exists rs].
   by constructor; split_ands'; try (rewrite /= -(associative _) Hpst').
 Qed.
-Lemma wsat_update_gst n E σ r rf m1 (P : iCMRA Σ → Prop) :
+Lemma wsat_update_gst n E σ r rf m1 (P : iGst Σ → Prop) :
   m1 ≼{S n} gst r → m1 ⇝: P →
   wsat (S n) E σ (r ⋅ rf) → ∃ m2, wsat (S n) E σ (update_gst m2 r ⋅ rf) ∧ P m2.
 Proof.