diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 27872076ef9b0018501b78eca54cc59a3030d7e4..d8802008bcdfe212b74306f73e0d7b8e9b552dc4 100644
--- a/theories/typing/shr_bor.v
+++ b/theories/typing/shr_bor.v
@@ -55,7 +55,7 @@ Section typing.
   Lemma tctx_reborrow_shr E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [TCtx_hasty p (&shr{κ}ty)]
-                  [TCtx_hasty p (&shr{κ'}ty); TCtx_guarded p κ (&shr{κ}ty)].
+                  [TCtx_hasty p (&shr{κ'}ty); TCtx_blocked p κ (&shr{κ}ty)].
   Proof.
     iIntros (Hκκ' tid ??) "#LFT HE HL H".
     iDestruct (elctx_interp_persist with "HE") as "#HE'".
diff --git a/theories/typing/type_context.v b/theories/typing/type_context.v
index 7223a7f6842e276ae12eb71c4541b40265816203..26c9a78b1f168f744de6d60e53f23bd5cf51e88e 100644
--- a/theories/typing/type_context.v
+++ b/theories/typing/type_context.v
@@ -21,13 +21,13 @@ Section type_context.
 
   Inductive tctx_elt : Type :=
   | TCtx_hasty (p : path) (ty : type)
-  | TCtx_guarded (p : path) (κ : lft) (ty : type).
+  | TCtx_blocked (p : path) (κ : lft) (ty : type).
   Definition tctx := list tctx_elt.
 
   Definition tctx_elt_interp (tid : thread_id) (x : tctx_elt) : iProp Σ :=
     match x with
     | TCtx_hasty p ty => ∃ v, ⌜eval_path p = Some v⌝ ∗ ty.(ty_own) tid [v]
-    | TCtx_guarded p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
+    | TCtx_blocked p κ ty => ∃ v, ⌜eval_path p = Some v⌝ ∗
                              ([†κ] ={⊤}=∗ ▷ ty.(ty_own) tid [v])
     end%I.
   Definition tctx_interp (tid : thread_id) (T : tctx) : iProp Σ :=
@@ -83,7 +83,7 @@ Section type_context.
 
   Definition deguard_tctx_elt κ x :=
     match x with
-    | TCtx_guarded p κ' ty =>
+    | TCtx_blocked p κ' ty =>
       if decide (κ = κ') then TCtx_hasty p ty else x
     | _ => x
     end.
diff --git a/theories/typing/uniq_bor.v b/theories/typing/uniq_bor.v
index 1600c4b016d9d8408a1ba65b58b28210eda4d9b3..6a40cf91d101def65c0a06d8df1ffd3c2fc0e5e9 100644
--- a/theories/typing/uniq_bor.v
+++ b/theories/typing/uniq_bor.v
@@ -105,7 +105,7 @@ Section typing.
 
   Lemma tctx_borrow E L p n ty κ :
     tctx_incl E L [TCtx_hasty p (own n ty)]
-                  [TCtx_hasty p (&uniq{κ}ty); TCtx_guarded p κ (own n ty)].
+                  [TCtx_hasty p (&uniq{κ}ty); TCtx_blocked p κ (own n ty)].
   Proof.
     iIntros (tid ??) "#LFT $ $ H".
     rewrite /tctx_interp big_sepL_singleton big_sepL_cons big_sepL_singleton.
@@ -120,7 +120,7 @@ Section typing.
   Lemma tctx_reborrow_uniq E L p ty κ κ' :
     lctx_lft_incl E L κ' κ →
     tctx_incl E L [TCtx_hasty p (&uniq{κ}ty)]
-                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_guarded p κ (&uniq{κ}ty)].
+                  [TCtx_hasty p (&uniq{κ'}ty); TCtx_blocked p κ (&uniq{κ}ty)].
   Proof.
     iIntros (Hκκ' tid ??) "#LFT HE HL H".
     iDestruct (elctx_interp_persist with "HE") as "#HE'".