From 0010b710c8576319e12593b6009de4fad8098633 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 23 Mar 2020 18:16:56 +0100
Subject: [PATCH] Params for `iProto_le`.

---
 theories/channel/proto_channel.v | 1 +
 1 file changed, 1 insertion(+)

diff --git a/theories/channel/proto_channel.v b/theories/channel/proto_channel.v
index b8e2245..6ba6365 100644
--- a/theories/channel/proto_channel.v
+++ b/theories/channel/proto_channel.v
@@ -216,6 +216,7 @@ Proof. solve_contractive. Qed.
 Definition iProto_le `{invG Σ} (p1 p2 : iProto Σ) : iProp Σ :=
   fixpoint iProto_le_aux p1 p2.
 Arguments iProto_le {_ _} _%proto _%proto.
+Instance: Params (@iProto_le) 2 := {}.
 
 Fixpoint proto_interp {Σ} (vs : list val) (p1 p2 : iProto Σ) : iProp Σ :=
   match vs with
-- 
GitLab