diff --git a/CHANGELOG.md b/CHANGELOG.md index baa924f03902faad3331dd42951266189d6c5043..2b37214d146d6153e98ec3794ee6f988751b01a2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -90,7 +90,9 @@ sed 's/\bPersistentP\b/Persistent/g; s/\bTimelessP\b/Timeless/g; s/\bCMRADiscret + The version of big operations over lists was redefined so that it enjoys more definitional equalities. * Various improvements to `solve_ndisj`. -* Improve handling of pure (non-state-dependent) reductions in heap_lang. +* Some extensions/improvements of heap_lang: + - Improve handling of pure (non-state-dependent) reductions. + - Add fetch-and-add (`FAA`) operation. * Use `Hint Mode` to prevent Coq from making arbitrary guesses in the presence of evars, which often led to divergence. There are a few places where type annotations are now needed.