diff --git a/CHANGELOG.md b/CHANGELOG.md index dd1775bc2a33910e14a38c33e2853c40788bead1..3f7293efdb1c6d74f94e0fbb2b624a76fd03049c 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -207,7 +207,9 @@ 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: `|={Eo,Ei}â–·=> P`. New: `|={Eo}[Ei]â–·=> P`. + Here, `Eo` is the "outer mask" (used at the beginning and end) and `Ei` the + "inner mask" (used around the â–· in the middle). As part of this, the lemmas about the 3-mask variant were changed to be about the 2-mask variant instead, and `step_fupd_mask_mono` now also has a more consistent argument order for its masks.