rename TCtx_guarded to TCtx_blocked

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'".

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.

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'".