From 86b442684cc3497add869b933657f8932c86e166 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 21 Aug 2020 16:59:46 +0200
Subject: [PATCH] Fixed bugs

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

diff --git a/theories/channel/channel.v b/theories/channel/channel.v
index d394efa..2cc7027 100644
--- a/theories/channel/channel.v
+++ b/theories/channel/channel.v
@@ -112,7 +112,7 @@ Notation "c ↣ p" := (iProto_mapsto c p)
 
 Instance iProto_mapsto_contractive `{!heapG Σ, !chanG Σ} c :
   Contractive (iProto_mapsto c).
-Proof. rewrite iProto_mapsto_eq. solve_contractive.
+Proof. rewrite iProto_mapsto_eq. solve_contractive. Qed.
 
 Definition iProto_choice {Σ} (a : action) (P1 P2 : iProp Σ)
     (p1 p2 : iProto Σ) : iProto Σ :=
diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 70a07db..ef7dd6f 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -268,6 +268,11 @@ Arguments iProto_le {_ _} _%proto _%proto.
 Instance: Params (@iProto_le) 2 := {}.
 Notation "p ⊑ q" := (iProto_le p q) : bi_scope.
 
+Instance iProto_le_ne {Σ V} : NonExpansive2 (@iProto_le Σ V).
+Proof. solve_proper. Qed.
+Instance iProto_le_proper {Σ V} : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
+Proof. solve_proper. Qed.
+
 Fixpoint iProto_interp_aux {Σ V} (n : nat)
     (vsl vsr : list V) (pl pr : iProto Σ V) : iProp Σ :=
   match n with
@@ -544,10 +549,6 @@ Section proto.
   Lemma iProto_le_unfold p1 p2 : iProto_le p1 p2 ≡ iProto_le_pre iProto_le p1 p2.
   Proof. apply: (fixpoint_unfold iProto_le_pre'). Qed.
 
-  Global Instance iProto_le_ne : NonExpansive2 (@iProto_le Σ V).
-  Proof. solve_proper. Qed.
-  Global Instance iProto_le_proper : Proper ((≡) ==> (≡) ==> (⊣⊢)) (@iProto_le Σ V).
-  Proof. solve_proper. Qed.
   Global Instance iProto_le_is_except_0 p1 p2 : IsExcept0 (p1 ⊑ p2).
   Proof.
     rewrite /IsExcept0 /bi_except_0. iIntros "[H|$]".
-- 
GitLab