From df0f72f02c7b469851f7a24750fbf72ba3bc79d1 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 11 Dec 2017 09:32:52 +0100
Subject: [PATCH] changelog
---
CHANGELOG.md | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/CHANGELOG.md b/CHANGELOG.md
index 6b056c827..751a9cea7 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,8 @@ Coq development, but not every API-breaking change is listed. Changes marked
Changes in and extensions of the theory:
-* Add new modality: â– ("plainly").
+* [Experimental feature] Add new modality: â– ("plainly").
+* Define `uPred` as a quotient on monotone predicates `M -> SProp`.
* Camera morphisms have to be homomorphisms, not just monotone functions.
* Add a proof that `f` has a fixed point if `f^k` is contractive.
* Constructions for least and greatest fixed points over monotone predicates
--
GitLab