From e6356d68ae94c2cdf5fe0d0b6f3fb43854f6c02b Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Fri, 1 May 2020 10:53:08 +0200
Subject: [PATCH] Bumped master

---
 theories/logrel/session_types.v | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index cb8dcc2..8289817 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -64,19 +64,14 @@ Section session_types.
   Global Instance lty_msg_exist_proper k :
     Proper (pointwise_relation _ (≡) ==> (≡)) (@lty_msg_exist Σ k).
   Proof. solve_proper. Qed.
-  Global Instance lty_msg_base_ne a : NonExpansive2 (@lty_msg_base Σ a).
+  Global Instance lty_msg_base_ne : NonExpansive2 (@lty_msg_base Σ).
   Proof. rewrite /lty_msg_base. solve_proper. Qed.
-  Global Instance lty_msg_base_proper a :
-    Proper ((≡) ==> (≡) ==> (≡)) (@lty_msg_base Σ a).
+  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 :
     Proper (dist_later n ==> dist_later n ==> dist n) (@lty_msg_base Σ).
-  Proof.
-    intros A1 A2 HA S1 S2 HS.
-    rewrite /lty_msg_base.
-    f_equiv=> w.
-    by repeat f_contractive.
-  Qed.
+  Proof. solve_contractive. Qed.
 
   Global Instance lty_message_ne a : NonExpansive (@lty_message Σ a).
   Proof. solve_proper. Qed.
-- 
GitLab