From ea9f230a7bbe4e56462e698e6340b3cb4cb0c94b Mon Sep 17 00:00:00 2001 From: Ralf Jung <jung@mpi-sws.org> Date: Mon, 26 Jul 2021 08:57:03 +0000 Subject: [PATCH] Update CHANGELOG --- CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/CHANGELOG.md b/CHANGELOG.md index 1b38eea02..897bc5fe1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -67,6 +67,7 @@ Coq 8.11 is no longer supported in this version of Iris. * 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. + (by Hai Dang, BedRock Systems) **Changes in `proofmode`:** -- GitLab