From 0d29e9f8c24055629da8af06c19b10ec897e52f7 Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Mon, 14 Sep 2020 17:00:57 +0200
Subject: [PATCH] Uncurried contractiveness of lty_msg_base, and added
 contractive of lty_chan

---
 theories/logrel/session_types.v | 4 ++--
 theories/logrel/term_types.v    | 2 ++
 2 files changed, 4 insertions(+), 2 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 8466ecb..c932551 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -94,8 +94,8 @@ Section session_types.
   Global Instance lty_msg_base_proper :
     Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ).
   Proof. rewrite /lty_msg_base. apply ne_proper_2, _. Qed.
-  Global Instance lty_msg_base_contractive n A :
-    Proper (dist_later n ==> dist n) (@lty_msg_base Σ A).
+  Global Instance lty_msg_base_contractive n :
+    Proper (dist n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
   Proof. solve_contractive. Qed.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
diff --git a/theories/logrel/term_types.v b/theories/logrel/term_types.v
index b2ab312..c630722 100644
--- a/theories/logrel/term_types.v
+++ b/theories/logrel/term_types.v
@@ -157,6 +157,8 @@ Section term_types.
   Global Instance lty_ref_shr_ne `{heapG Σ} : NonExpansive lty_ref_shr.
   Proof. solve_proper. Qed.
 
+  Global Instance lty_chan_contractive `{heapG Σ, chanG Σ} : Contractive lty_chan.
+  Proof. solve_contractive. Qed.
   Global Instance lty_chan_ne `{heapG Σ, chanG Σ} : NonExpansive lty_chan.
   Proof. solve_proper. Qed.
 End term_types.
-- 
GitLab