From 54fecc1ed5d8c021455f7f8c6571fca919d27398 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Thu, 15 Oct 2020 22:25:08 +0200
Subject: [PATCH] CHANGELOG.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1d11d3930..59ed387ae 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -49,6 +49,8 @@ With this release, we dropped support for Coq 8.9.
 * Move the `*_validI` and `*_equivI` lemmas to a new module, `base_logic.algebra`.
   That module is exported by `base_logic.base_logic` so it should usually be
   available everywhere without further changes.
+* The authoritative fragment `✓ (◯ b : auth A)` is no longer definitionally
+  equal to `✓ b`.
 
 **Changes in `proofmode`:**
 
-- 
GitLab