From add4702b1223ec539bd7e33c05d199d505e04129 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Fri, 25 Nov 2016 18:32:44 +0100
Subject: [PATCH] update CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 24b30199d..89bbb9efa 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -16,6 +16,8 @@ Coq development, but not every API-breaking change is listed.  Changes marked
   recursive domain equation.  As a consequence, CMRAs no longer need a proof
   of completeness.
   (The old `cofeT` is provided by `algebra.deprecated`.)
+* [#] Implement a new agreement construction.  Unlike the old one, this one
+  preserves discreteness.
 * Renaming and moving things around: uPred and the rest of the base logic are
   in `base_logic`, while `program_logic` is for everything involving the
   general Iris notion of a language.
-- 
GitLab