From d4654827ca6b70ed531be3236150550ee89c4c0f Mon Sep 17 00:00:00 2001
From: jihgfee <jihgfee@gmail.com>
Date: Tue, 24 Nov 2020 10:39:45 +0100
Subject: [PATCH] Added missing variable to fix CI failure

---
 theories/channel/proto.v | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/theories/channel/proto.v b/theories/channel/proto.v
index 9d1fb7b..93341be 100644
--- a/theories/channel/proto.v
+++ b/theories/channel/proto.v
@@ -359,12 +359,14 @@ Section proto.
   Global Instance iMsg_car_proper :
     Proper (iMsg_equiv ==> (=) ==> (≡) ==> (≡)) (iMsg_car (Σ:=Σ) (V:=V)).
   Proof.
-    iIntros (m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+    intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+    f_equiv; [ by f_equiv | done ].
   Qed.
-  Global Instance iMsg_car_ne :
+  Global Instance iMsg_car_ne n :
     Proper (iMsg_dist n ==> (=) ==> (dist n) ==> (dist n)) (iMsg_car (Σ:=Σ) (V:=V)).
   Proof.
-    iIntros (n m1 m2 meq v1 v2 veq p1 p2 peq). rewrite meq. by do 2 f_equiv=> //.
+    intros m1 m2 meq v1 v2 veq p1 p2 peq. rewrite meq.
+    f_equiv; [ by f_equiv | done ].
   Qed.
 
   Global Instance iMsg_contractive v n :
-- 
GitLab