From f2be354358291bc3dbd3640d976a58c0a623a08e Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sun, 4 Oct 2020 02:12:11 +0200
Subject: [PATCH] Rename `cmra_monotone_valid` into `cmra_morphism_valid`.

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

diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index e284e59dd..de26c43e8 100644
--- a/theories/algebra/cmra.v
+++ b/theories/algebra/cmra.v
@@ -769,7 +769,7 @@ Section cmra_morphism.
   Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
   Lemma cmra_morphism_monotoneN n x y : x ≼{n} y → f x ≼{n} f y.
   Proof. intros [z ->]. exists (f z). by rewrite cmra_morphism_op. Qed.
-  Lemma cmra_monotone_valid x : ✓ x → ✓ f x.
+  Lemma cmra_morphism_valid x : ✓ x → ✓ f x.
   Proof. rewrite !cmra_valid_validN; eauto using cmra_morphism_validN. Qed.
 End cmra_morphism.
 
-- 
GitLab