CHANGELOG.

CHANGELOG.md

@@ -19,6 +19,9 @@ lemma.
 * Change statement of `Z_local_update` to be more intuitive. It now says
   `x - y = x' - y' → (x,y) ~l~> (x',y')`, i.e., the difference between the
   authoritative element and the fragment must stay the same.
+* Rename `cmra_discrete_update` → `cmra_discrete_total_update` and
+  `cmra_discrete_updateP` → `cmra_discrete_total_updateP`. Repurpose original
+  names for lemmas that only require `CmraDiscrete`, not `CmraTotal`.
 
 **Changes in `proofmode`:**
 
@@ -29,6 +32,17 @@ lemma.
   `MaybeFrame` class has become notation for `TCNoBackTrack (MaybeFrame' ...)`,
   which means the proofs of your instances might need a slight refactoring.
 
+The following `sed` script helps adjust your code to the renaming (on macOS,
+replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`).
+Note that the script is not idempotent, do not run it twice.
+```
+sed -i -E -f- $(find theories -name "*.v") <<EOF
+# discrete camera updates
+s/\bcmra_discrete_update\b/cmra_discrete_total_update/g
+s/\bcmra_discrete_updateP\b/cmra_discrete_total_updateP/g
+EOF
+```
+
 ## Iris 4.1.0 (2023-10-11)
 
 This Iris release mostly features quality-of-life improvements, such as smarter