From a9fa2606ee6c7ddbf658e44d4ddbb9ddd5f40124 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Mon, 3 May 2021 12:55:32 +0200
Subject: [PATCH] CHANGELOG.

---
 CHANGELOG.md | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index ebe3c7c3..5556ab79 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,6 +19,16 @@ API-breaking change is listed.
     longer work for multisets.
 - Make `Qc_of_Z'` not an implicit coercion (from `Z` to `Qc`) any more.
 - Make `Z.of_nat'` not an implicit coercion (from `nat` to `Z`) any more.
+- Rename `decide_left` → `decide_True_pi` and `decide_right` → `decide_False_pi`.
+
+The following `sed` script should perform most of the renaming
+(on macOS, replace `sed` by `gsed`, installed via e.g. `brew install gnu-sed`):
+```
+sed -i -E '
+s/\bdecide_left\b/decide_True_pi/g
+s/\bdecide_right\b/decide_False_pi/g
+' $(find theories -name "*.v")
+```
 
 ## std++ 1.5.0
 
-- 
GitLab