From 73dd71dc7cffc6a4ffb90a45a236748148e3c188 Mon Sep 17 00:00:00 2001
From: Ralf Jung <jung@mpi-sws.org>
Date: Mon, 14 Sep 2020 18:03:45 +0200
Subject: [PATCH] add a sed script

---
 CHANGELOG.md | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 3f5aebcf2..d82399af9 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -7,7 +7,8 @@ lemma.
 
 **Changes in `algebra`:**
 
-* Rename `agree_op_{inv,invL}'` to `to_agree_op_{inv,inv_L}`, and add
+* Rename `agree_op_inv'` to `to_agree_op_inv`,
+  `agree_op_invL'` to `to_agree_op_inv_L`, and add
   `to_agree_op_invN`.
 * Rename `auth_auth_frac_op_invL` to `auth_auth_frac_op_inv_L`,
   `excl_auth_agreeL` to `excl_auth_agree_L`,
@@ -29,6 +30,19 @@ lemma.
   pure facts rather than the previous default of `a`. This also requires some
   changes if you were implementing `FromForall`, in order to forward names.
 
+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
+# agree and L suffix renames
+s/\bagree_op_inv'\b/to_agree_op_inv/g
+s/\bagree_op_invL'\b/to_agree_op_inv_L/g
+s/\bauth_auth_frac_op_invL\b/auth_auth_frac_op_inv_L/g
+s/\b(excl|frac|ufrac)_auth_agreeL/\1_auth_agree_L/g
+EOF
+```
+
 ## Iris 3.3.0 (released 2020-07-15)
 
 This release does not have any outstanding highlights, but contains a large
-- 
GitLab