From 6e29397ba96dab748d881ad37e443327a84a6042 Mon Sep 17 00:00:00 2001
From: Jacques-Henri Jourdan <jacques-henri.jourdan@normalesup.org>
Date: Mon, 26 Dec 2016 14:21:09 +0100
Subject: [PATCH] =?UTF-8?q?Really,=20the=20notation=20for=20the=20local=20?=
 =?UTF-8?q?lifetime=20context=20should=20be=20=E2=8A=91.?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

---
 theories/typing/lft_contexts.v | 6 +++---
 theories/typing/programs.v     | 4 ++--
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/theories/typing/lft_contexts.v b/theories/typing/lft_contexts.v
index c927125a..9ac50908 100644
--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -27,7 +27,7 @@ Definition llctx := list llctx_elt.
 Delimit Scope lrust_llctx_scope with LL.
 Bind Scope lrust_llctx_scope with llctx llctx_elt.
 
-Notation "κ ⊐ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
+Notation "κ ⊑ κl" := (@pair lft (list lft) κ κl) (at level 70) : lrust_llctx_scope.
 
 Notation "a :: b" := (@cons llctx_elt a%LL b%LL)
   (at level 60, right associativity) : lrust_llctx_scope.
@@ -165,7 +165,7 @@ Section lft_contexts.
   Lemma lctx_lft_incl_static κ : lctx_lft_incl κ static.
   Proof. iIntros "_ _". iApply lft_incl_static. Qed.
 
-  Lemma lctx_lft_incl_local κ κ' κs : (κ ⊐ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
+  Lemma lctx_lft_incl_local κ κ' κs : (κ ⊑ κs)%LL ∈ L → κ' ∈ κs → lctx_lft_incl κ κ'.
   Proof.
     iIntros (? Hκ'κs) "_ H". iDestruct "H" as %HL.
     edestruct HL as [κ0 EQ]. done. simpl in EQ; subst.
@@ -193,7 +193,7 @@ Section lft_contexts.
   Qed.
 
   Lemma lctx_lft_alive_local κ κs:
-    (κ ⊐ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
+    (κ ⊑ κs)%LL ∈ L → Forall lctx_lft_alive κs → lctx_lft_alive κ.
   Proof.
     iIntros ([i HL]%elem_of_list_lookup_1 Hκs F qE qL ?) "HE HL".
     iDestruct "HL" as "[HL1 HL2]". rewrite {2}/llctx_interp /llctx_elt_interp.
diff --git a/theories/typing/programs.v b/theories/typing/programs.v
index f84f0d1b..440f4e81 100644
--- a/theories/typing/programs.v
+++ b/theories/typing/programs.v
@@ -95,7 +95,7 @@ Section typing_rules.
 
   Lemma typed_newlft E L C T κs e :
     Closed [] e →
-    (∀ κ, typed_body E ((κ ⊐ κs) :: L) C T e) →
+    (∀ κ, typed_body E ((κ ⊑ κs) :: L) C T e) →
     typed_body E L C T (Newlft ;; e).
   Proof.
     iIntros (Hc He tid qE) "#HEAP #LFT Htl HE HL HC HT".
@@ -110,7 +110,7 @@ Section typing_rules.
      Right now, we could take two. *)
   Lemma typed_endlft E L C T1 T2 κ κs e :
     Closed [] e → UnblockTctx κ T1 T2 →
-    typed_body E L C T2 e → typed_body E ((κ ⊐ κs) :: L) C T1 (Endlft ;; e).
+    typed_body E L C T2 e → typed_body E ((κ ⊑ κs) :: L) C T1 (Endlft ;; e).
   Proof.
     iIntros (Hc Hub He tid qE) "#HEAP #LFT Htl HE". rewrite /llctx_interp big_sepL_cons.
     iIntros "[Hκ HL] HC HT". iDestruct "Hκ" as (Λ) "(% & Htok & #Hend)".
-- 
GitLab