From 46595d5c6b4bf266f239cf162924369014173c1e Mon Sep 17 00:00:00 2001
From: Dan Frumin <dan@groupoid.moe>
Date: Thu, 30 Dec 2021 14:58:40 +0000
Subject: [PATCH] `Later_inj` -> `Next_inj`.

---
 CHANGELOG.md       | 1 +
 iris/algebra/ofe.v | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d29a6eea1..6fb5027e7 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 f6119fe6a..57ef8b7c7 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.
-- 
GitLab