diff --git a/CHANGELOG.md b/CHANGELOG.md
index 1b38eea0282f2e6154b9ffc170bd3932cb5b8eef..897bc5fe115f2e43aa9e7f4be762064b4680a2f9 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`:**