From 36f40743bd99bb74e624580673e564fc1fef488c Mon Sep 17 00:00:00 2001
From: jihgfee <jkas@itu.dk>
Date: Fri, 27 Mar 2020 13:29:26 +0100
Subject: [PATCH] Added some laters in premises

---
 theories/channel/channel.v | 2 +-
 theories/channel/proto.v   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index c8e4886..6e4bb0c 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -131,7 +131,7 @@ Section channel.
   Global Instance iProto_mapsto_proper c : Proper ((≡) ==> (≡)) (iProto_mapsto c).
   Proof. apply (ne_proper _). Qed.
 
-  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ iProto_le p1 p2 -∗ c ↣ p2.
+  Lemma iProto_mapsto_le c p1 p2 : c ↣ p1 -∗ ▷ iProto_le p1 p2 -∗ c ↣ p2.
   Proof.
     rewrite iProto_mapsto_eq. iDestruct 1 as (γ s l r lk ->) "[Hlk H]".
     iIntros "Hle'". iExists γ, s, l, r, lk. iSplit; [done|]. iFrame "Hlk".
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 29cd3db..7e62cb5 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -867,7 +867,7 @@ Section proto.
   Proof. apply (ne_proper _). Qed.
 
   Lemma iProto_own_le γ s p1 p2 :
-    iProto_own γ s p1 -∗ iProto_le p1 p2 -∗ iProto_own γ s p2.
+    iProto_own γ s p1 -∗ ▷ iProto_le p1 p2 -∗ iProto_own γ s p2.
   Proof.
     iDestruct 1 as (p1') "[Hle H]". iIntros "Hle'".
     iExists p1'. iFrame "H". by iApply (iProto_le_trans with "Hle").
-- 
GitLab