From b48c3b16846b4058b3225431945cf0eeba6d9895 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Mon, 31 May 2021 12:57:49 +0200
Subject: [PATCH] Disambiguate agree_op_proper (noticed when trying to give a
 mode to Equiv)

---
 iris/algebra/agree.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/iris/algebra/agree.v b/iris/algebra/agree.v
index 2421f8332..306eb8a8d 100644
--- a/iris/algebra/agree.v
+++ b/iris/algebra/agree.v
@@ -121,7 +121,7 @@ Proof.
 Qed.
 Local Instance agree_op_ne : NonExpansive2 (@op (agree A) _).
 Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
-Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) op := ne_proper_2 _.
+Local Instance agree_op_proper : Proper ((≡) ==> (≡) ==> (≡)) (op (A := agree A)) := ne_proper_2 _.
 
 Lemma agree_included x y : x ≼ y ↔ y ≡ x ⋅ y.
 Proof.
-- 
GitLab