From 8d4ba814bd97a865c5722563846b312eb447ff4c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 12 Aug 2022 08:29:15 -0400
Subject: [PATCH] better naming

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

diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index 1b61b0be8..e74c57758 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -311,7 +311,7 @@ Section limit_preserving.
 
   (** This is strictly weaker than the [_impl] variant, but sometimes automation
       is better at proving [Proper] for [iff] than for [impl]. *)
-  Lemma limit_preserving_iff (P1 P2 : A → Prop) :
+  Lemma limit_preserving_impl' (P1 P2 : A → Prop) :
     Proper (dist 0 ==> iff) P1 →
     LimitPreserving P2 →
     LimitPreserving (λ x, P1 x → P2 x).
-- 
GitLab