diff --git a/CHANGELOG.md b/CHANGELOG.md
index ee1ebd372aaa209f3b431c9d8b7d85df7696a5bd..11847299e92c7bfe34c23d6828a1acafe2bfd1d8 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -173,7 +173,10 @@ API-breaking change is listed.
 - 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`. (by Paolo G. Giarrusso, BedRock Systems)
+  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)
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).