diff --git a/iris/base_logic/lib/iprop.v b/iris/base_logic/lib/iprop.v
index 16babcffa4db27f2f66fd15a2db9a02cf5a256e1..a9fb90a627fd85b5626afb6aaeeb45a6a438ee86 100644
--- a/iris/base_logic/lib/iprop.v
+++ b/iris/base_logic/lib/iprop.v
@@ -32,6 +32,8 @@ Global Arguments GFunctor _ {_}.
 Global Existing Instance gFunctor_map_contractive.
 Add Printing Constructor gFunctor.
 
+Notation GFunctorConst F := (GFunctor (constRF F)).
+
 (** The type [gFunctors] describes the parameters [Σ] of the Iris logic: lists
 of [gFunctor]s.
 
diff --git a/iris_heap_lang/lib/rw_spin_lock.v b/iris_heap_lang/lib/rw_spin_lock.v
index c2e60ea52953d1b0249dee98963e485688e34e9d..d49923099f808db6e72361fb9f20713a795bcb6a 100644
--- a/iris_heap_lang/lib/rw_spin_lock.v
+++ b/iris_heap_lang/lib/rw_spin_lock.v
@@ -33,10 +33,10 @@ Local Definition acquire_writer : val :=
 Local Definition release_writer : val :=
   λ: "l", "l" <- #0.
 
-Class rwlockG Σ := RwLockG { rwlock_tokG : inG Σ (authR (gmultisetUR Qp)) }.
+Class rwlockG Σ := RwLockG { rwlock_tokG : inG Σ (auth (gmultiset Qp)) }.
 Local Existing Instance rwlock_tokG.
 
-Local Definition rwlockΣ : gFunctors := #[GFunctor (authR (gmultisetUR Qp)) ].
+Local Definition rwlockΣ : gFunctors := #[GFunctorConst (auth (gmultiset Qp)) ].
 Global Instance subG_rwlockΣ {Σ} : subG rwlockΣ Σ → rwlockG Σ.
 Proof. solve_inG. Qed.
 
diff --git a/iris_heap_lang/lib/spawn.v b/iris_heap_lang/lib/spawn.v
index 0d5fea58c918e521d8bec9f891b24b7475691889..40c739e26653ea48e0ab7bd62e56455fd9699ca9 100644
--- a/iris_heap_lang/lib/spawn.v
+++ b/iris_heap_lang/lib/spawn.v
@@ -19,10 +19,10 @@ Definition join : val :=
 
 (** The CMRA & functor we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (exclR unitO) }.
+Class spawnG Σ := SpawnG { spawn_tokG : inG Σ (excl ()) }.
 Local Existing Instance spawn_tokG.
 
-Definition spawnΣ : gFunctors := #[GFunctor (exclR unitO)].
+Definition spawnΣ : gFunctors := #[GFunctorConst (excl ())].
 
 Global Instance subG_spawnΣ {Σ} : subG spawnΣ Σ → spawnG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris_heap_lang/lib/spin_lock.v b/iris_heap_lang/lib/spin_lock.v
index 5218861f67f12bacd01b328b58611ca4f89225a1..62ca5d3b2fa38a827857aec2eca54a48616eebc2 100644
--- a/iris_heap_lang/lib/spin_lock.v
+++ b/iris_heap_lang/lib/spin_lock.v
@@ -14,10 +14,10 @@ Definition release : val := λ: "l", "l" <- #false.
 
 (** The CMRA we need. *)
 (* Not bundling heapGS, as it may be shared with other users. *)
-Class lockG Σ := LockG { lock_tokG : inG Σ (exclR unitO) }.
+Class lockG Σ := LockG { lock_tokG : inG Σ (excl ()) }.
 Local Existing Instance lock_tokG.
 
-Definition lockΣ : gFunctors := #[GFunctor (exclR unitO)].
+Definition lockΣ : gFunctors := #[GFunctorConst (excl ())].
 
 Global Instance subG_lockΣ {Σ} : subG lockΣ Σ → lockG Σ.
 Proof. solve_inG. Qed.
diff --git a/iris_heap_lang/lib/ticket_lock.v b/iris_heap_lang/lib/ticket_lock.v
index 0827bcd7d169db1154cc33c86009124dbee11de4..c286e8947035131f72019ad3636d9967452a44b1 100644
--- a/iris_heap_lang/lib/ticket_lock.v
+++ b/iris_heap_lang/lib/ticket_lock.v
@@ -28,11 +28,11 @@ Definition release : val :=
 
 (** The CMRAs we need. *)
 Class tlockG Σ :=
-  tlock_G : inG Σ (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))).
+  tlock_G : inG Σ (auth (excl' nat * gset_disj nat)).
 Local Existing Instance tlock_G.
 
 Definition tlockΣ : gFunctors :=
-  #[ GFunctor (authR (prodUR (optionUR (exclR natO)) (gset_disjUR nat))) ].
+  #[ GFunctorConst (auth (excl' nat * gset_disj nat)) ].
 
 Global Instance subG_tlockΣ {Σ} : subG tlockΣ Σ → tlockG Σ.
 Proof. solve_inG. Qed.
@@ -45,14 +45,14 @@ Section proof.
     ∃ o n : nat,
       lo ↦ #o ∗ ln ↦ #n ∗
       own γ (● (Excl' o, GSet (set_seq 0 n))) ∗
-      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε, GSet {[ o ]}))).
+      ((own γ (◯ (Excl' o, GSet ∅)) ∗ R) ∨ own γ (◯ (ε : excl' _, GSet {[ o ]}))).
 
   Definition is_lock (γ : gname) (lk : val) (R : iProp Σ) : iProp Σ :=
     ∃ lo ln : loc,
       ⌜lk = (#lo, #ln)%V⌝ ∗ inv N (lock_inv γ lo ln R).
 
   Definition issued (γ : gname) (x : nat) : iProp Σ :=
-    own γ (◯ (ε, GSet {[ x ]})).
+    own γ (◯ (ε : excl' _, GSet {[ x ]})).
 
   Definition locked (γ : gname) : iProp Σ := ∃ o, own γ (◯ (Excl' o, GSet ∅)).