From bd689fffc36c12778528faf264f25c5ca387e46b Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Thu, 3 Aug 2023 19:24:59 +0200
Subject: [PATCH] rename

---
 iris/algebra/cmra.v | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/iris/algebra/cmra.v b/iris/algebra/cmra.v
index 53cbcdbd9..4b14550a1 100644
--- a/iris/algebra/cmra.v
+++ b/iris/algebra/cmra.v
@@ -1546,9 +1546,9 @@ Section option.
     rewrite /included. f_equiv=> mc. by rewrite -(inj_iff Some b) Some_op_opM.
   Qed.
 
-  Lemma Some_validN_includedN n a b : ✓{n} a → Some b ≼{n} Some a → ✓{n} b.
+  Lemma cmra_validN_Some_includedN n a b : ✓{n} a → Some b ≼{n} Some a → ✓{n} b.
   Proof. apply: (cmra_validN_includedN _ (Some _) (Some _)). Qed.
-  Lemma Some_valid_included a b : ✓ a → Some b ≼ Some a → ✓ b.
+  Lemma cmra_valid_Some_included a b : ✓ a → Some b ≼ Some a → ✓ b.
   Proof. apply: (cmra_valid_included (Some _) (Some _)). Qed.
 
   Lemma Some_includedN_total `{!CmraTotal A} n a b : Some a ≼{n} Some b ↔ a ≼{n} b.
-- 
GitLab