From 024bb001cd2a51d067644de18beafc4572779683 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Wed, 26 May 2021 00:09:37 +0200
Subject: [PATCH] More CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 91836201..36f0f130 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -22,6 +22,13 @@ API-breaking change is listed.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
 - Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
 - Add `option_guard_True_pi`.
+- Add lemma `surjective_finite` (by Alix Trieu).
+- Add type classes `TCFalse`, `TCUnless`, `TCExists`, and `TCFastDone` (by
+  Michael Sammler).
+- Add various results about bit representations of `Z` (by Michael Sammler).
+- Add tactic `learn_hyp` (by Michael Sammler).
+- Add `Countable` instance for decidable Sigma types (by Simon Gregersen).
+- Add tactics `compute_done` and `compute_by` for solving goals by computation.
 
 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