diff --git a/CHANGELOG.md b/CHANGELOG.md
index 701c609d412b27e1343939aa3d987b4b5890e909..83b1c86158fde7498e2745e65801a7566f664644 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -34,10 +34,14 @@ Changes in and extensions of the theory:
 * [#] heap_lang values are now injected in heap_lang expressions via a specific
   constructor of the expr inductive type. This simplifies much the tactical
   infrastructure around the language. In particular, this allow us to get rid
-  the reflexion mechanism that was needed for proving closedness, atomicity and
+  the reflection mechanism that was needed for proving closedness, atomicity and
   "valueness" of a term. The price to pay is the addition of new
   "administrative" reductions in the operational semantics of the language.
-
+* [#] Extend the state interpretation with a natural number that keeps track of
+  the number of forked-off threads, and have a global fixed proposition that
+  describes the postcondition of each forked-off thread (instead of it being
+  `True`). Additionally, there is a stronger variant of the adequacy theorem
+  that allows to make use of the postconditions of the forked-off threads.
 
 Changes in Coq: