rename mgmtE -> lftE

theories/typing/own.v

@@ -52,7 +52,7 @@ Section own.
                    ▷ freeable_sz n ty.(ty_size) l)%I;
        ty_shr κ tid E l :=
          (∃ l':loc, &frac{κ}(λ q', l ↦{q'} #l') ∗
-            □ (∀ F q, ⌜E ∪ mgmtE ⊆ F⌝ -∗ q.[κ] ={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∗ q.[κ]))%I
+            □ (∀ F q, ⌜E ∪ lftE ⊆ F⌝ -∗ q.[κ] ={F,F∖E∖↑lftN}▷=∗ ty.(ty_shr) κ tid E l' ∗ q.[κ]))%I
     |}.
   Next Obligation.
     iIntros (q ty tid vl) "H". iDestruct "H" as (l) "[% _]". by subst.

theories/typing/type.v

@@ -10,7 +10,7 @@ Class typeG Σ := TypeG {
   type_frac_borrowG Σ :> frac_borG Σ
 }.
 
-Definition mgmtE := ↑lftN.
+Definition lftE := ↑lftN.
 Definition lrustN := nroot .@ "lrust".
 
 Section type.
@@ -39,7 +39,7 @@ Section type.
          nicer (they would otherwise require a "∨ □|=>[†κ]"), and (b) so that
          we can have emp == sum [].
        *)
-      ty_share E N κ l tid q : mgmtE ⊥ ↑N → mgmtE ⊆ E →
+      ty_share E N κ l tid q : lftE ⊥ ↑N → lftE ⊆ E →
         lft_ctx -∗ &{κ} (l ↦∗: ty_own tid) -∗ q.[κ] ={E}=∗
         ty_shr κ tid (↑N) l ∗ q.[κ];
       ty_shr_mono κ κ' tid E E' l : E ⊆ E' →
@@ -50,7 +50,7 @@ Section type.
   Class Copy (t : type) := {
     copy_persistent tid vl : PersistentP (t.(ty_own) tid vl);
     copy_shr_acc κ tid E F l q :
-      mgmtE ∪ F ⊆ E →
+      lftE ∪ F ⊆ E →
       lft_ctx -∗ t.(ty_shr) κ tid F l -∗
         q.[κ] ∗ na_own tid F ={E}=∗ ∃ q', ▷l ↦∗{q'}: t.(ty_own) tid ∗
           (▷l ↦∗{q'}: t.(ty_own) tid ={E}=∗ q.[κ] ∗ na_own tid F)

theories/typing/typing.v

@@ -80,7 +80,7 @@ Section typing.
   Qed.
 
   Definition consumes (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ ↑lrustN ⊆ E →
+    ∀ ν tid Φ E, lftE ∪ ↑lrustN ⊆ E →
       lft_ctx -∗ ρ1 ν tid -∗ na_own tid ⊤ -∗
       (∀ (l:loc) vl q,
         (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗{q} vl ∗
@@ -100,7 +100,7 @@ Section typing.
   Qed.
 
   Definition update (ty : type) (ρ1 ρ2 : expr → perm) : Prop :=
-    ∀ ν tid Φ E, mgmtE ∪ (↑lrustN) ⊆ E →
+    ∀ ν tid Φ E, lftE ∪ (↑lrustN) ⊆ E →
       lft_ctx -∗ ρ1 ν tid -∗
       (∀ (l:loc) vl,
          (⌜length vl = ty.(ty_size)⌝ ∗ ⌜eval_expr ν = Some #l⌝ ∗ l ↦∗ vl ∗

theories/typing/uniq_bor.v

@@ -16,7 +16,7 @@ Section uniq_bor.
          (∃ (l:loc) P, (⌜vl = [ #l ]⌝ ∗ □ (P ↔ l ↦∗: ty.(ty_own) tid)) ∗ &{κ} P)%I;
        ty_shr κ' tid E l :=
          (∃ l':loc, &frac{κ'}(λ q', l ↦{q'} #l') ∗
-            □ ∀ F q, ⌜E ∪ mgmtE ⊆ F⌝ -∗ q.[κ∪κ']
+            □ ∀ F q, ⌜E ∪ lftE ⊆ F⌝ -∗ q.[κ∪κ']
                 ={F, F∖E∖↑lftN}▷=∗ ty.(ty_shr) (κ∪κ') tid E l' ∗ q.[κ∪κ'])%I
     |}.
   Next Obligation.