From ff1aafac4c98c4193f988f66ca9ed4e304564a9c Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Wed, 28 Jul 2021 15:16:49 +0200
Subject: [PATCH] changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 9314f0c3..eb55cc22 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -153,6 +153,8 @@ API-breaking change is listed.
   `difference_insert`, `difference_insert_subseteq`. (by Hai Dang)
 - Tweak reduction on `gset`, so that `cbn` matches the behavior by `simpl` and
   does not unfold `gset` operations. (by Paolo G. Giarrusso, BedRock Systems)
+- Add `get_head` tactic to determine the syntactic head of a function
+  application term.
 
 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