From c1d2615aada1277280ff03da8a751e82313c9c13 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 5 Nov 2021 08:29:25 +0100
Subject: [PATCH] CHANGELOG: Unnest, and mention compatibility

---
 CHANGELOG.md | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 11847299..cc074bf6 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -172,11 +172,11 @@ API-breaking change is listed.
   equal.
 - Add lemma `choose_proper` showing that `choose P` respects predicate
   equivalence. (by Paolo G. Giarrusso, BedRock Systems)
-- Well-founded definitions: Add induction principle `Acc_dep_ind`, a dependent
-  version of `Acc_ind`. This lives in a new module `well_founded` together with
-  some things that were previously found in `relations`: `Acc_impl`, `wf_guard`,
-  `wf_guard`, `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
-  (by Paolo G. Giarrusso, BedRock Systems)
+- Extract module `well_founded` from `relations`, and re-export it for
+  compatibility. This contains `Acc_impl`, `wf_guard`, `wf_guard`,
+  `wf_projected`, `Fix_F_proper`, `Fix_unfold_rel`.
+- Add induction principle `relations.Acc_dep_ind`, a dependent
+  version of `Acc_ind`. (by Paolo G. Giarrusso, BedRock Systems)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
-- 
GitLab