From 7d8bf699090e01710da0a6eb40b38f6712784ef4 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 11 Jun 2021 00:17:19 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 80799303..ad6707e0 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -68,6 +68,11 @@ API-breaking change is listed.
   + Generalize lemmas `partial_alter_merge`, `partial_alter_merge_l`, and
     `partial_alter_merge_r`.
   + Drop unused `merge_assoc'` instance.
+- Improvements to `head` and `tail` functions for lists:
+  + Define `head` as notation that prints (Coq defines it as `parsing only`)
+    similar to `tail`.
+  + 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`):
-- 
GitLab