diff --git a/CHANGELOG.md b/CHANGELOG.md
index d29a6eea1ed174550b05750579313740c0edf6fd..6fb5027e7a25492796c7f90e5f6c57346702ecb7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,7 @@ lemma.
 * Equip `frac_agree` with support for `dfrac` and rename it to `dfrac_agree`.
   The old `to_frac_agree` and its lemmas still exist, except that the
   `frac_agree_op_valid` lemmas are made bi-directional.
+* Rename typeclass instance `Later_inj` -> `Next_inj`.
 
 **Changes in `bi`:**
 
diff --git a/iris/algebra/ofe.v b/iris/algebra/ofe.v
index f6119fe6a183df7bd15ca96913e56a33537a5310..57ef8b7c74cbee86d38df4cb8f0922b3c4769edc 100644
--- a/iris/algebra/ofe.v
+++ b/iris/algebra/ofe.v
@@ -1170,7 +1170,7 @@ Section later.
 
   Global Instance Next_contractive : Contractive (@Next A).
   Proof. by intros [|n] x y. Qed.
-  Global Instance Later_inj n : Inj (dist n) (dist (S n)) (@Next A).
+  Global Instance Next_inj n : Inj (dist n) (dist (S n)) (@Next A).
   Proof. by intros x y. Qed.
 
   Lemma Next_uninj x : ∃ a, x ≡ Next a.