CHANGELOG.

CHANGELOG.md

@@ -61,6 +61,10 @@ API-breaking change is listed.
 - Rename instances `option_mbind_proper` → `option_bind_proper` and
   `option_mjoin_proper` → `option_join_proper` to be consistent with similar
   instances for sets and lists.
+- Improvements to `head` and `tail` functions for lists:
+  + Define `head` as notation that prints (Coq defines it as `parsing only`).
+  + Declare `tail` as `simpl nomatch`.
+  + Add lemmas about `head` and `tail`.
 
 The following `sed` script should perform most of the renaming
 (on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):