From 02c439a0682ff6ca3e4b02b5c7efc530d2723582 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Tue, 14 Jul 2020 10:18:28 +0200
Subject: [PATCH] changelog: consistent metavariables

---
 CHANGELOG.md | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd1775bc2..3f7293efd 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.
-- 
GitLab