From 05ebd4df77b18a117cdfd4c5566ed41cd1049331 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Aug 2024 16:21:57 +0200
Subject: [PATCH] avoid naming a typeclass argument

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

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index ab9189f10..203e73dc6 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1727,7 +1727,7 @@ Section discrete_fun_cmra.
     by intros [h Hh]; exists (h x); rewrite /op /discrete_fun_op_instance (Hh x).
   Qed.
 
-  Lemma discrete_fun_included_spec `{Hfin : Finite A} (f g : discrete_fun B) :
+  Lemma discrete_fun_included_spec `{Finite A} (f g : discrete_fun B) :
     f ≼ g ↔ ∀ x, f x ≼ g x.
   Proof.
     split; [by intros; apply discrete_fun_included_spec_1|].
-- 
GitLab