Tweak comments and CHANGELOG.

CHANGELOG.md

@@ -13,7 +13,8 @@ API-breaking change is listed.
 - Make the build script compatible with BSD systems. (by Yiyun Liu)
 - Rename lemmas `X_length` into `length_X`, see the sed script below for an
   overview. This follows https://github.com/coq/coq/pull/18564.
-- Redefine `map_imap` so it can be used in nested recursive `Fixpoint`s.
+- Redefine `map_imap` so its closure argument can contain recursive
+  occurrences of a `Fixpoint`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).

tests/fin_maps.v

@@ -435,7 +435,8 @@ Proof. discriminate. Qed.
 Goal GTest {[ GTest {[ 1 := GTest ∅ ]} := GTest ∅ ]} ≠@{gtest (gtest nat)} GTest ∅.
 Proof. discriminate. Qed.
 
-(* Test that [map_imap] can be used in nested recursive fixpoints. *)
+(* Test that a fixpoint can be recursively invoked in the closure argument
+of [map_imap]. *)
 Fixpoint gtest_imap `{Countable K} (j : K) (t : gtest K) : gtest K :=
   let '(GTest ts) := t in
   GTest (map_imap (λ i t, guard (i = j);; Some (gtest_imap j t)) ts).