set release date to tomorrow, re-flow changelog

CHANGELOG.md

@@ -3,32 +3,30 @@ way the logic is used on paper.  We also document changes in the Coq
 development; every API-breaking change should be listed, but not every new
 lemma.
 
-## Iris 4.0.0 (2022-08-??)
+## Iris 4.0.0 (2022-08-18)
 
-The highlight of this release is the *later credits* mechanism, which
-provides a new way to eliminate later modalities.
+The highlight of Iris 4.0 is the *later credits* mechanism, which provides a new
+way to eliminate later modalities.
 
 This new mechanism complements the existing techniques of taking program steps,
-exploiting timelessness, and various modality commuting rules.
-At each program step, one obtains a credit `£ 1`, which is an
-ownable Iris resource. These credits don't have to be used at the present step,
-but can be saved up, and used to eliminate laters at any point in the
-verification using the fancy update modality.
-Later credits are particularly
-useful in proofs where there is not a one-to-one correspondence between program
-steps and later eliminations, for example, logical atomicity proofs.
-As a consequence, we have been able to simplify the definition of logical atomicity
-by removing the 'laterable' mechanism.
+exploiting timelessness, and various modality commuting rules. At each program
+step, one obtains a credit `£ 1`, which is an ownable Iris resource. These
+credits don't have to be used at the present step, but can be saved up, and used
+to eliminate laters at any point in the verification using the fancy update
+modality. Later credits are particularly useful in proofs where there is not a
+one-to-one correspondence between program steps and later eliminations, for
+example, logical atomicity proofs. As a consequence, we have been able to
+simplify the definition of logical atomicity by removing the 'laterable'
+mechanism.
 
 The later credit mechanism is described in detail in the
-[ICFP'22 paper](https://plv.mpi-sws.org/later-credits/)
-and there is a
+[ICFP'22 paper](https://plv.mpi-sws.org/later-credits/) and there is a
 [small tutorial](https://gitlab.mpi-sws.org/iris/iris/-/blob/master/tests/later_credits_paper.v)
-in the Iris repository.
-The [examples](https://gitlab.mpi-sws.org/iris/examples/) repository contains
-some logically atomic case studies that make use of later credits:
-the counter with a backup (Section 4 of the later credits paper), as well as
-the elimination stack, conditional increment, and RDCSS.
+in the Iris repository. The
+[examples](https://gitlab.mpi-sws.org/iris/examples/) repository contains some
+logically atomic case studies that make use of later credits: the counter with a
+backup (Section 4 of the later credits paper), as well as the elimination stack,
+conditional increment, and RDCSS.
 
 Iris 4.0 supports Coq 8.13 - 8.16.