From 69e9e8d243b9c5d69c2e762d467817fd1fe59e4a Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 17 Nov 2020 14:28:57 +0100
Subject: [PATCH] Add all instance arguments, needed for compilation with
 recent Coq.

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

diff --git a/theories/logrel/session_types.v b/theories/logrel/session_types.v
index 0d78227..1a79e7d 100644
--- a/theories/logrel/session_types.v
+++ b/theories/logrel/session_types.v
@@ -83,7 +83,7 @@ Hint Mode LtyMsgTele ! - ! - - : typeclass_instances.
 Section session_types.
   Context {Σ : gFunctors}.
 
-  Global Instance lty_msg_exist_ne k :
+  Global Instance lty_msg_exist_ne k n :
     Proper (pointwise_relation _ (dist n) ==> (dist n)) (@lty_msg_exist Σ k).
   Proof. solve_proper. Qed.
   Global Instance lty_msg_exist_proper k :
@@ -107,11 +107,11 @@ Section session_types.
   Proof. solve_proper. Qed.
   Global Instance lty_choice_proper a : Proper ((≡) ==> (≡)) (@lty_choice Σ a).
   Proof. apply ne_proper, _. Qed.
-  Global Instance lty_choice_contractive a :
+  Global Instance lty_choice_contractive a n :
     Proper (map_relation (dist_later n) (λ _, False) (λ _, False) ==> dist n)
            (@lty_choice Σ a).
   Proof.
-    intros n Ss Ts Heq. rewrite /lty_choice.
+    intros Ss Ts Heq. rewrite /lty_choice.
     do 2 f_equiv. f_equiv => i.
     rewrite !lookup_total_alt.
     specialize (Heq i).
diff --git a/theories/logrel/subtyping.v b/theories/logrel/subtyping.v
index 2b94498..69acaac 100644
--- a/theories/logrel/subtyping.v
+++ b/theories/logrel/subtyping.v
@@ -34,7 +34,7 @@ Section subtyping.
   Global Instance lty_bi_le_plain {k} (M1 M2 : lty Σ k) : Plain (M1 <:> M2).
   Proof. rewrite /lty_bi_le /=. apply _. Qed.
 
-  Global Instance lty_le_ne : NonExpansive2 (@lty_le Σ k).
+  Global Instance lty_le_ne k : NonExpansive2 (@lty_le Σ k).
   Proof. destruct k; solve_proper. Qed.
   Global Instance lty_le_proper {k} : Proper ((≡) ==> (≡) ==> (≡)) (@lty_le Σ k).
   Proof. apply (ne_proper_2 _). Qed.
-- 
GitLab