From ba7879fc44e8e27cdeaa43b928402ed8becd4ab4 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 16 Mar 2020 16:24:32 +0100
Subject: [PATCH] vdash changelog

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 7685b229b..d3277110e 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -21,6 +21,10 @@ Coq development, but not every API-breaking change is listed.  Changes marked
 **Changes in Coq:**
 
 * Added support for Coq 8.10 and Coq 8.11; dropped support for Coq 8.7 and Coq 8.8.
+* Removed coercion from `iProp` (and other MoSeL propositions) to `Prop`.
+  Instead, use the new unary notation `⊢ P`, or `⊢@{PROP} P` if the proposition
+  type cannot be inferred. This also means that `%I` should not be necessary any
+  more when stating lemmas, as `P` above is automatically parsed in scope `%I`.
 * A new tactic `iStopProof` to turn the proof mode entailment into an ordinary
   Coq goal `big star of context ⊢ proof mode goal`.
 * Rename `iProp`/`iPreProp` to `iPropO`/`iPrePropO` since they are `ofeT`s.
-- 
GitLab