From 7a3374e8a356e0e5ea31694ad35bacfc489b1418 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Thu, 15 Dec 2016 18:17:53 +0100
Subject: [PATCH] rename TCtx_guarded to TCtx_blocked

---
 theories/typing/shr_bor.v      | 2 +-
 theories/typing/type_context.v | 6 +++---
 theories/typing/uniq_bor.v     | 4 ++--
 3 files changed, 6 insertions(+), 6 deletions(-)

diff --git a/theories/typing/shr_bor.v b/theories/typing/shr_bor.v
index 27872076..d8802008 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 7223a7f6..26c9a78b 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 1600c4b0..6a40cf91 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'".
-- 
GitLab