diff --git a/CHANGELOG.md b/CHANGELOG.md
index c2d9876df853248565f1ee21d483881c950572a3..586806bef79ff0e9a74ba5dfd5394d3c5ec65b50 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -38,6 +38,8 @@ With this release, we dropped support for Coq 8.9.
   `auth_auth_valid*`, `auth_frag_valid*`, or `auth_both_valid*` instead.
 * Add the camera of discardable fractions `dfrac`. This is a generalization of
   the normal fractional camera. See `theories/algebra/dfrac.v` for further information.
+* Rename `cmra_monotone_valid` into `cmra_morphism_valid` (this rename was
+  forgotten in !56).
 
 **Changes in `proofmode`:**
 
diff --git a/theories/algebra/cmra.v b/theories/algebra/cmra.v
index e284e59dd1f8a891fb8472952252a9ad474f0a49..de26c43e83cafe89f47559b88c6e051cc0f1ab5c 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.