diff --git a/CHANGELOG.md b/CHANGELOG.md index f18c74dd5aa8ab673403b2a92c343d41a13711dd..21375bfb0d0e78a504d5bc8a8b94b6bd96fec5c1 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -207,7 +207,7 @@ Coq development, but not every API-breaking change is listed. Changes marked numbers`. * Remove notation for 3-mask step-taking updates, and made 2-mask notation less confusing by distinguishing it better from mask-changing updates. - Old: `|={E1,E2]â–·=> P`. New: `|={Eo}[Ei]â–·=> P`. + Old: `|={E1,E2}â–·=> P`. New: `|={Eo}[Ei]â–·=> P`. As part of this, the lemma `step_fupd_mask_mono` now also has a more consistent argument order for its masks.