diff --git a/program_logic/iris.v b/program_logic/iris.v
index b32b16f073864c36a099365719db9410c4b9be96..8269a5982cd453b9cd25b11edcf28bebd834ac67 100644
--- a/program_logic/iris.v
+++ b/program_logic/iris.v
@@ -3,10 +3,10 @@ From iris.prelude Require Export coPset.
 From iris.algebra Require Import gmap auth agree gset coPset upred_big_op.
 
 Class irisPreG (Λ : language) (Σ : gFunctors) : Set := IrisPreG {
-  state_inG :> inG Σ (authUR (optionUR (exclR (stateC Λ))));
-  invariant_inG :> inG Σ (authUR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
-  enabled_inG :> inG Σ coPset_disjUR;
-  disabled_inG :> inG Σ (gset_disjUR positive);
+  state_inG :> inG Σ (authR (optionUR (exclR (stateC Λ))));
+  invariant_inG :> inG Σ (authR (gmapUR positive (agreeR (laterC (iPreProp Σ)))));
+  enabled_inG :> inG Σ coPset_disjR;
+  disabled_inG :> inG Σ (gset_disjR positive);
 }.
 
 Class irisG (Λ : language) (Σ : gFunctors) : Set := IrisG {
diff --git a/program_logic/thread_local.v b/program_logic/thread_local.v
index f37c90474f2d80fea35cb1d038e706bbe56d980f..b7619d4e9eb90df700248fddba3821976efa8f15 100644
--- a/program_logic/thread_local.v
+++ b/program_logic/thread_local.v
@@ -5,7 +5,7 @@ Import uPred.
 Definition thread_id := gname.
 
 Class thread_localG Σ :=
-  tl_inG :> inG Σ (prodUR coPset_disjUR (gset_disjUR positive)).
+  tl_inG :> inG Σ (prodR coPset_disjR (gset_disjR positive)).
 
 Definition tlN : namespace := nroot .@ "tl".
 
@@ -47,7 +47,7 @@ Section proofs.
     â–· P ={E}=> tl_inv tid N P.
   Proof.
     iIntros "HP".
-    iVs (own_empty tid) as "Hempty".
+    iVs (own_empty (A:=prodUR coPset_disjUR (gset_disjUR positive)) tid) as "Hempty".
     iVs (own_updateP with "Hempty") as ([m1 m2]) "[Hm Hown]".
     { apply prod_updateP'. apply cmra_updateP_id, (reflexivity (R:=eq)).
       apply (gset_alloc_empty_updateP_strong' (λ i, i ∈ nclose N)).