From f7e06e4d225ef728d3e1fe10b04407a8bb308f13 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Fri, 20 Mar 2020 11:24:04 +0100
Subject: [PATCH] CHANGELOG entry.

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d3277110e..d10badce4 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -78,6 +78,7 @@ Coq development, but not every API-breaking change is listed.  Changes marked
    `not_stuck_fill` → `not_stuck_fill_inv`.
   - Use the non-`_inv` names (that freed up) for the forwards directions:
    `reducible_fill`, `reducible_no_obs_fill`, `irreducible_fill_inv`.
+* The tactic `iAssumption` also recognizes assumptions `⊢ P` in the Coq context.
 
 **Changes in heap_lang:**
 
-- 
GitLab