From af309491b5dd2bfd8781e4934ff4641704be4153 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 21 May 2019 13:49:12 +0200
Subject: [PATCH] expand CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index fa3956dff..28c4f0b84 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -67,6 +67,8 @@ Changes in Coq:
 * The `iInv` tactic can now be used without the second argument (the name for
   the closing update).  It will then instead add the obligation to close the
   invariant to the goal.
+* The new `iEval` tactic can be used to execute a simplification or rewriting
+  tactic on some specific part(s) of the proofmode goal.
 * Added support for defining derived connectives involving n-ary binders using
   telescopes.
 * The proof mode now more consistently "prettifies" the goal after each tactic.
@@ -109,6 +111,7 @@ Changes in Coq:
 * Remove locked value lambdas. The value scope notations `rec: f x := e` and
   `(λ: x, e)` no longer add a `locked`. Instead, we made the `wp_` tactics
   smarter to no longer unfold lambdas/recs that occur behind definitions.
+* Export the fact that `iPreProp` is a COFE.
 
 ## Iris 3.1.0 (released 2017-12-19)
 
-- 
GitLab