From 195389f08f1e9acea02daed445fc9fc50e876a69 Mon Sep 17 00:00:00 2001
From: Hoang-Hai Dang <haidang@mpi-sws.org>
Date: Wed, 30 Jun 2021 19:29:40 +0200
Subject: [PATCH] Add CHANGELOG

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

diff --git a/CHANGELOG.md b/CHANGELOG.md
index d8478647c..1b38eea02 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -64,6 +64,9 @@ Coq 8.11 is no longer supported in this version of Iris.
   - Use `□`/`-∗` instead of `<pers>`/`→`.
   - Strengthen to ensure that functions for recursive calls are non-expansive.
 * Add `big_andM` (big conjunction on finite maps) with lemmas similar to `big_andL`.
+* Add transitive embedding that constructs an embedding of `PROP1` into `PROP3`
+  by combining the embeddings of `PROP1` into `PROP2` and `PROP2` into `PROP3`.
+  This construct is *not* declared as an instance to avoid TC search divergence.
 
 **Changes in `proofmode`:**
 
-- 
GitLab